-Compare the new definitions of `add` and `div` closely: the definition
-for `add` shows what it looks like to equip an ordinary operation to
-survive in a presupposition-filled world, and the definition of `div`
-shows exactly what extra needs to be added in order to trigger the
-no-division-by-zero presupposition.
+Compare the new definitions of `add'` and `div'` closely: the definition
+for `add'` shows what it looks like to equip an ordinary operation to
+survive in dangerous presupposition-filled world. Note that the new
+definition of `add'` does not need to test whether its arguments are
+None objects or real numbers---those details are hidden inside of the
+`bind'` function.