--- a/QuotMain.thy	Sat Dec 05 23:35:09 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 00:00:47 2009 +0100
@@ -1105,10 +1105,9 @@
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
-    val thms1 = @{thms all_prs ex_prs}
+    val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-                @ defs
     fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
     (* FIXME: use of someting smaller than HOL_basic_ss *)
   in