--- a/QuotMain.thy	Wed Nov 11 10:22:47 2009 +0100
+++ b/QuotMain.thy	Wed Nov 11 18:49:46 2009 +0100
@@ -839,17 +839,27 @@
 
 section {* Cleaning the goal *}
 
-lemma prod_fun_id: "prod_fun id id = id"
-by (simp add: prod_fun_def)
+lemma prod_fun_id: "prod_fun id id \<equiv> id"
+by (rule eq_reflection) (simp add: prod_fun_def)
 
-lemma map_id: "map id x = x"
-by (induct x) (simp_all)
+lemma map_id: "map id \<equiv> id"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (rule_tac list="x" in list.induct)
+apply (simp_all)
+done
 
 ML {*
 fun simp_ids lthy thm =
-  thm
-  |> MetaSimplifier.rewrite_rule @{thms id_def_sym}
-  |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id}
+  MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
+*}
+
+ML {*
+fun simp_ids_trm trm =
+  trm |>
+  MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+  |> cprop_of |> Thm.dest_equals |> snd
+
 *}
 
 text {* expects atomized definition *}