--- a/Quot/quotient_tacs.ML	Mon Feb 08 06:27:20 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 08 10:47:19 2010 +0100
@@ -649,16 +649,15 @@
 end
 
 (* An Attribute which automatically constructs the qthm *)
-(* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *)
 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
-  val goal_chk = Syntax.check_term ctxt goal
-  val frees = Term.add_free_names goal_chk []
+  val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
+  val goal = (quotient_lift_all ctxt o prop_of) thm'
+  val nthm = Goal.prove ctxt [] [] goal (fn x => lift_tac ctxt [thm] 1)
+  val [nthm1] = ProofContext.export ctxt' ctxt [nthm]
 in
-  Goal.prove ctxt frees [] goal_chk 
-   (fn x => lift_tac (#context x) [thm] 1)
+  nthm1
 end;
 
 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux