diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 01 23:59:32 2010 +0100
@@ -72,7 +72,7 @@
       TVar _ => mk_Free rty
     | Type (_, []) => mk_identity rty
     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
-    | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)")
+    | _ => raise LIFT_MATCH ("mk_mapfun (default)")
 in
   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
@@ -120,13 +120,13 @@
 
 (* produces an aggregate absrep function                           *)
 (*                                                                 *)
-(* - In case of equal types we just return the identity            *)
+(* - In case of equal types we just return the identity.           *)
 (*                                                                 *)
 (* - In case of function types and TFrees, we recurse, taking in   *) 
 (*   the first case the polarity change into account.              *)
 (*                                                                 *)
 (* - If the type constructors are equal, we recurse for the        *)
-(*   arguments and prefix the appropriate map function             *)
+(*   arguments and build the appropriate map function.             *)
 (*                                                                 *)
 (* - If the type constructors are unequal, there must be an        *)
 (*   instance of quotient types:                                   *)
@@ -135,12 +135,12 @@
 (*       must be some distinct TVars                               *)  
 (*     - we then match the rty_pat with rty and qty_pat with qty;  *)
 (*       if matching fails the types do not match                  *)
-(*     - the matching produces two environments, we look up the    *)
+(*     - the matching produces two environments; we look up the    *)
 (*       assignments for the qty_pat variables and recurse on the  *)
-(*       assignmetnts                                              *)
+(*       assignments                                               *)
 (*     - we prefix the aggregate map function for the rty_pat,     *)
 (*       which is an abstraction over all type variables           *)
-(*     - finally we compse the result with the appropriate         *)
+(*     - finally we compose the result with the appropriate        *)
 (*       absrep function                                           *)    
 (*                                                                 *)
 (*   The composition is necessary for types like                   *)