# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265712032 -3600
# Node ID 6961fda38e09a07424da6a9a2dc301f11a2b2ecf
# Parent  66097fe4942a0fb66f7d503d66e7f9d94916ed71
minor tuning

diff -r 66097fe4942a -r 6961fda38e09 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Mon Feb 08 13:50:52 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Feb 09 11:40:32 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 *)