--- a/QuotMain.thy	Tue Oct 27 16:15:56 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 17:08:47 2009 +0100
@@ -786,18 +786,27 @@
     val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
     val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
   in
-    Simplifier.rewrite_rule [rt] thm
+    @{thm Pure.equal_elim_rule1} OF [rt,thm]
   end
 *}
 
+ML {*
+  fun repeat_eqsubst_thm ctxt thms thm =
+    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+    handle _ => thm
+*}
+
 text {* expects atomized definition *}
 ML {*
   fun add_lower_defs_aux ctxt thm =
     let
-      val e1 = @{thm fun_cong} OF [thm]
-      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1
+      val e1 = @{thm fun_cong} OF [thm];
+      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1;
+      val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f;
+      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g;
+      val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h
     in
-      thm :: (add_lower_defs_aux ctxt f)
+      thm :: (add_lower_defs_aux ctxt i)
     end
     handle _ => [thm]
 *}