# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257961919 -3600
# Node ID e39c8793a23333760b1a57c355410c69c289b570
# Parent  9aa3aba71ecc679345737645cfb2762f7d99b38a# Parent  e7279efbe3dda6c6f4307e158f91a0a8824b81db
merge

diff -r e7279efbe3dd -r e39c8793a233 QuotMain.thy
--- a/QuotMain.thy	Wed Nov 11 11:59:22 2009 +0100
+++ b/QuotMain.thy	Wed Nov 11 18:51:59 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 *}
diff -r e7279efbe3dd -r e39c8793a233 quotient_def.ML
--- a/quotient_def.ML	Wed Nov 11 11:59:22 2009 +0100
+++ b/quotient_def.ML	Wed Nov 11 18:51:59 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;