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