--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 24 15:08:05 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 24 22:38:45 2010 +0800
@@ -686,8 +686,8 @@
rthm
|> asm_full_simplify ss
|> Drule.eta_contraction_rule
- val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
- val goal = derive_qtrm ctxt qtys (prop_of rthm'')
+ val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
+ val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
in
Goal.prove ctxt' [] [] goal
(K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))