--- a/Quot/quotient_tacs.ML	Fri Feb 05 15:17:21 2010 +0100
+++ b/Quot/quotient_tacs.ML	Sat Feb 06 10:04:56 2010 +0100
@@ -15,7 +15,7 @@
   val lift_tac: Proof.context -> thm list -> int -> tactic
   val quotient_tac: Proof.context -> int -> tactic
   val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
-  val lifted_attr: attribute
+  val lifted_attrib: attribute
 end;
 
 structure Quotient_Tacs: QUOTIENT_TACS =
@@ -648,15 +648,19 @@
   THEN' RANGE (map mk_tac rthms)
 end
 
-(* The attribute *)
-fun lifted_attr_pre ctxt thm =
+(* An Attribute *)
+(* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *)
+fun lifted_attrib_pre context thm =
 let
-  val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
-  val glc = Syntax.check_term ctxt gl
+  val ctxt = Context.proof_of context
+  val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
+  val goal_chk = Syntax.check_term ctxt goal
+  val frees = Term.add_free_names goal_chk []
 in
-  (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1))
+  Goal.prove ctxt frees [] goal_chk 
+   (fn x => lift_tac (#context x) [thm] 1)
 end;
 
-val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t)
+val lifted_attrib = Thm.rule_attribute lifted_attrib_pre
 
 end; (* structure *)