--- 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 *}

--- a/quotient_def.ML	Wed Nov 11 10:22:47 2009 +0100
+++ b/quotient_def.ML	Wed Nov 11 18:49:46 2009 +0100
@@ -10,6 +10,7 @@
     local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
     local_theory -> local_theory
+  val diff: (typ * typ) -> (typ * typ) list -> (typ * typ) list
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -176,4 +177,4 @@
 
 end; (* structure *)
 
-open Quotient_Def;
\ No newline at end of file
+open Quotient_Def;