# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265631200 -3600
# Node ID 480324a48a1c507695c8aaa6d2165f430a207c83
# Parent  bb7f4457091a78d2b9f6e585c07cf3a5ec2b5867# Parent  ab5789ad8d7d8cd557892e5d7758591d58729b43
merged

diff -r bb7f4457091a -r 480324a48a1c Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Mon Feb 08 13:12:55 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Feb 08 13:13:20 2010 +0100
@@ -689,23 +689,14 @@
 
 (*** Wrapper for transforming an rthm into a qthm ***)
 
-(*
-Finds subterms of a term that can be lifted and:
-
-* replaces subterms matching lifted constants by the lifted constants
-
-* replaces equivalence relations by equalities
-
-* In constants, frees and schematic variables replaces
-  subtypes matching lifted types by those types 
-*)
-
+(* 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 =
   if r <> NONE then r else
   case try (Sign.typ_match thy (ty, rty)) Vartab.empty of
     SOME inst => SOME (Envir.subst_type inst qty)
   | NONE => NONE
-
 fun subst_tys thy substs ty =
   case fold (subst_ty thy ty) substs NONE of
     SOME ty => ty
@@ -714,14 +705,20 @@
         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
       | x => x)
 
+(* 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. *)
 fun subst_trm thy t (rtrm, qtrm) s =
   if s <> NONE then s else
     case try (Pattern.match thy (t, rtrm)) (Vartab.empty, Vartab.empty) of
       SOME inst => SOME (Envir.subst_term inst qtrm)
     | NONE => NONE;
-
 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
 
+(* prepares type and term substitution pairs to be used by above
+   functions that let replace all raw constructs by appropriate
+   lifted counterparts. *)
 fun get_ty_trm_substs ctxt =
 let
   val thy = ProofContext.theory_of ctxt
@@ -735,6 +732,18 @@
   (ty_substs, const_substs @ rel_substs)
 end
 
+
+(*
+Finds subterms of a term that can be lifted and:
+
+* replaces subterms matching lifted constants by the lifted constants
+
+* replaces equivalence relations by equalities
+
+* In constants, frees and schematic variables replaces
+  subtypes matching lifted types by those types
+*)
+
 fun quotient_lift_all ctxt t =
 let
   val thy = ProofContext.theory_of ctxt