--- a/Quot/quotient_term.ML	Tue Feb 09 15:28:15 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 15:28:30 2010 +0100
@@ -687,9 +687,9 @@
 
 
 
-(*** Wrapper for transforming an rthm into a qthm ***)
+(*** Wrapper for automatically transforming an rthm into a qthm ***)
 
-(* subst_tys takes a list of (rty,qty) substitution pairs
+(* subst_tys takes a list of (rty, qty) substitution pairs
    and replaces all occurences of rty in the given type
    by appropriate qty, with substitution *)
 fun subst_ty thy ty (rty, qty) r =
@@ -705,7 +705,7 @@
         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
       | x => x)
 
-(* subst_trms takes a list of (rtrm,qtrm) substitution pairs
+(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
    and if the  given term matches any of the raw terms it
    returns the appropriate qtrm instantiated. If none of
    them matched it returns NONE. *)
@@ -722,9 +722,9 @@
 fun get_ty_trm_substs ctxt =
 let
   val thy = ProofContext.theory_of ctxt
-  val quot_infos = Quotient_Info.quotdata_dest ctxt
+  val quot_infos  = Quotient_Info.quotdata_dest ctxt
+  val const_infos = Quotient_Info.qconsts_dest ctxt
   val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
-  val const_infos = Quotient_Info.qconsts_dest ctxt
   val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
   fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
   val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
@@ -734,14 +734,14 @@
 
 
 (*
-Finds subterms of a term that can be lifted and:
+Takes a term and
 
-* replaces subterms matching lifted constants by the lifted constants
+* replaces raw constants by the quotient constants
 
 * replaces equivalence relations by equalities
 
-* In constants, frees and schematic variables replaces
-  subtypes matching lifted types by those types
+* replaces raw types by the quotient types
+
 *)
 
 fun quotient_lift_all ctxt t =
@@ -770,7 +770,6 @@
 end
 
 
-
 end; (* structure *)