--- a/Quot/QuotMain.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -1058,13 +1058,15 @@
     val thy = ProofContext.theory_of lthy;
     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 = defs @ (prs_rules_get lthy)
-    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} 
-                @ (id_simps_get lthy)
+    val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
+    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [simp_tac (simps thms1),
             fun_map_tac lthy,
+            fun_map_tac lthy,
+            fun_map_tac lthy,
+            fun_map_tac lthy,
             lambda_prs_tac lthy,
             simp_tac (simps thms2),
             TRY o rtac refl]