--- a/QuotMain.thy	Thu Oct 29 12:09:31 2009 +0100
+++ b/QuotMain.thy	Thu Oct 29 13:29:03 2009 +0100
@@ -870,6 +870,14 @@
 
 section {* Cleaning the goal *}
 
+lemma prod_fun_id: "prod_fun id id = id"
+  apply (simp add: prod_fun_def)
+done
+lemma map_id: "map id x = x"
+  apply (induct x)
+  apply (simp_all add: map.simps)
+done
+
 text {* expects atomized definition *}
 ML {*
   fun add_lower_defs_aux ctxt thm =
@@ -877,10 +885,9 @@
       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
+      val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g
     in
-      thm :: (add_lower_defs_aux ctxt i)
+      thm :: (add_lower_defs_aux ctxt h)
     end
     handle _ => [thm]
 *}