diff -r 0ff855a6ffb7 -r ce774af6b964 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 26 12:06:47 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 26 12:24:23 2010 +0100
@@ -486,7 +486,7 @@
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
         val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
-        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+        val ts = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} te
         val (insp, inst) =
           if ty_c = ty_d
           then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)