diff -r 57944c1ef728 -r aa157e957655 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 12:25:12 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 16:56:03 2009 +0100
@@ -91,6 +91,8 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
+ML {* print_mapsinfo @{context} *}
+
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient 
@@ -996,18 +998,18 @@
   end)  
 *}
 
-section {* General Shape of the Lifting Procedure *}
+section {* The General Shape of the Lifting Procedure *}
 
-(* - A is the original raw theorem                  *)
-(* - B is the regularized theorem                   *)
-(* - C is the rep/abs injected version of B         *) 
-(* - D is the lifted theorem                        *)
-(*                                                  *)
-(* - b is the regularization step                   *)
-(* - c is the rep/abs injection step                *)
-(* - d is the cleaning part                         *)
-(*                                                  *)
-(* the QUOT_TRUE premise records the lifted theorem *)
+(* - A is the original raw theorem                       *)
+(* - B is the regularized theorem                        *)
+(* - C is the rep/abs injected version of B              *) 
+(* - D is the lifted theorem                             *)
+(*                                                       *)
+(* - b is the regularization step                        *)
+(* - c is the rep/abs injection step                     *)
+(* - d is the cleaning part                              *)
+(*                                                       *)
+(* the QUOT_TRUE premise in c records the lifted theorem *)
 
 lemma lifting_procedure:
   assumes a: "A"