# HG changeset patch
# User haftmann
# Date 1242285394 -7200
# Node ID 1c64b0827ee899988b7c5e187f6cbb4731dfbbe4
# Parent  03a87478b89e40484dd238c11ef0761462710418
rewrite op = == eq handled by simproc

diff -r 03a87478b89e -r 1c64b0827ee8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu May 14 09:16:33 2009 +0200
+++ b/src/HOL/HOL.thy	Thu May 14 09:16:34 2009 +0200
@@ -1331,7 +1331,7 @@
     of Abs (_, _, t') => count_loose t' 0 <= 1
      | _ => true;
 in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct)
-  then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*)
+  then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
   else let (*Norbert Schirmer's case*)
     val ctxt = Simplifier.the_context ss;
     val thy = ProofContext.theory_of ctxt;
@@ -1775,6 +1775,13 @@
 end
 *}
 
+subsubsection {* Generic code generator preprocessor setup *}
+
+setup {*
+  Code_Preproc.map_pre (K HOL_basic_ss)
+  #> Code_Preproc.map_post (K HOL_basic_ss)
+*}
+
 subsubsection {* Equality *}
 
 class eq =
@@ -1788,7 +1795,7 @@
 lemma eq_refl: "eq x x \<longleftrightarrow> True"
   unfolding eq by rule+
 
-lemma equals_eq [code inline]: "(op =) \<equiv> eq"
+lemma equals_eq: "(op =) \<equiv> eq"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
 declare equals_eq [symmetric, code post]
@@ -1797,6 +1804,14 @@
 
 declare equals_eq [code]
 
+setup {*
+  Code_Preproc.map_pre (fn simpset =>
+    simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}]
+      (fn thy => fn _ => fn t as Const (_, T) => case strip_type T
+        of ((T as Type _) :: _, _) => SOME @{thm equals_eq}
+         | _ => NONE)])
+*}
+
 
 subsubsection {* Generic code generator foundation *}
 
@@ -1851,18 +1866,17 @@
   "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: eq)
 
-
 text {* Equality *}
 
 declare simp_thms(6) [code nbe]
 
-hide (open) const eq
-hide const eq
-
 setup {*
   Code_Unit.add_const_alias @{thm equals_eq}
 *}
 
+hide (open) const eq
+hide const eq
+
 text {* Cases *}
 
 lemma Let_case_cert:
@@ -1883,13 +1897,6 @@
 
 code_abort undefined
 
-subsubsection {* Generic code generator preprocessor *}
-
-setup {*
-  Code_Preproc.map_pre (K HOL_basic_ss)
-  #> Code_Preproc.map_post (K HOL_basic_ss)
-*}
-
 subsubsection {* Generic code generator target languages *}
 
 text {* type bool *}
diff -r 03a87478b89e -r 1c64b0827ee8 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu May 14 09:16:33 2009 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu May 14 09:16:34 2009 +0200
@@ -368,8 +368,7 @@
       addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
       addsimprocs [DatatypePackage.distinct_simproc]);
     fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
-      |> Simpdata.mk_eq
-      |> Simplifier.rewrite_rule [@{thm equals_eq}];
+      |> Simpdata.mk_eq;
   in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
 
 fun add_equality vs dtcos thy =