diff -r f3a24012e9d8 -r 86c7ed9f354f Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Dec 23 13:45:42 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 21:30:23 2009 +0100
@@ -287,8 +287,9 @@
   
   * If the application involves a bounded quantifier, we recurse on 
     the second argument. If the application is a bounded abstraction,
-    we always put an Re/Abs around it (since bounded abstractions
-    always need lifting). Otherwise we recurse on both arguments.
+    we always put an Rep/Abs around it (since bounded abstractions
+    are assumed to always need lifting). Otherwise we recurse on both 
+    arguments.
 
   For constants: