# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265457536 -3600
# Node ID f4da251473897a0acafbfbb7cd52af8b359d130e
# Parent  44461d5615eb02e148443dffe4fb739cd4894ab2
minor

diff -r 44461d5615eb -r f4da25147389 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Sat Feb 06 10:04:56 2010 +0100
+++ b/Quot/quotient_tacs.ML	Sat Feb 06 12:58:56 2010 +0100
@@ -648,9 +648,9 @@
   THEN' RANGE (map mk_tac rthms)
 end
 
-(* An Attribute *)
+(* An Attribute which automatically constructs the qthm *)
 (* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *)
-fun lifted_attrib_pre context thm =
+fun lifted_attrib_aux context thm =
 let
   val ctxt = Context.proof_of context
   val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
@@ -661,6 +661,6 @@
    (fn x => lift_tac (#context x) [thm] 1)
 end;
 
-val lifted_attrib = Thm.rule_attribute lifted_attrib_pre
+val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
 
 end; (* structure *)
diff -r 44461d5615eb -r f4da25147389 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Feb 06 10:04:56 2010 +0100
+++ b/Quot/quotient_term.ML	Sat Feb 06 12:58:56 2010 +0100
@@ -714,10 +714,10 @@
         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
       | x => x)
 
-fun subst_trm thy t (rt, qt) s =
+fun subst_trm thy t (rtrm, qtrm) s =
   if s <> NONE then s else
-    case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of
-      SOME inst => SOME (Envir.subst_term inst qt)
+    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