--- 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 *)