diff -r 3104d62e7a16 -r 119f7d6a3556 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Dec 17 14:58:33 2009 +0100
+++ b/Quot/quotient_info.ML	Thu Dec 17 17:59:12 2009 +0100
@@ -41,7 +41,7 @@
 (* data containers *)
 (*******************)
 
-(* info about map- and rel-functions *)
+(* info about map- and rel-functions for a type *)
 type maps_info = {mapfun: string, relfun: string}
 
 structure MapsData = Theory_Data
@@ -188,7 +188,7 @@
     | _ => raise NotFound
   end
 
-(* We don't print the definition *)
+(* We omit printing the definition *)
 fun print_qconstinfo ctxt =
 let
   fun prt_qconst {qconst, rconst, def} =
@@ -233,7 +233,7 @@
 
 val prs_rules_get = PrsRules.get
 
-(* respectfulness theorems *)
+(* id simplification theorems *)
 structure IdSimps = Named_Thms
   (val name = "id_simps"
    val description = "Identity simp rules for maps.")