--- a/Quot/QuotMain.thy	Tue Dec 08 16:56:51 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:35:04 2009 +0100
@@ -1056,8 +1056,7 @@
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
     val thms1 = @{thms all_prs ex_prs} @ defs
-    val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
-                @ @{thms Quotient_abs_rep Quotient_rel_rep} 
+    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [lambda_prs_tac lthy,