# HG changeset patch
# User haftmann
# Date 1276509690 -7200
# Node ID b5492f611129904a4fb8bbb80cb3edafe3bfe1b5
# Parent  ed431cc99f170f3a30d7ad015416f20344fc0fcf
explicitly name and note equations for class eq

diff -r ed431cc99f17 -r b5492f611129 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Jun 14 12:01:30 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Jun 14 12:01:30 2010 +0200
@@ -105,12 +105,14 @@
       in (thm', lthy') end;
     fun tac thms = Class.intro_classes_tac []
       THEN ALLGOALS (ProofContext.fact_tac thms);
+    fun prefix dtco = Binding.qualify true (Long_Name.base_name dtco) o Binding.qualify true "eq" o Binding.name;
     fun add_eq_thms dtco =
       Theory.checkpoint
       #> `(fn thy => mk_eq_eqns thy dtco)
-      #-> (fn (thms, thm) =>
-        Code.add_nbe_eqn thm
-        #> fold_rev Code.add_eqn thms);
+      #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
+          [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
+            ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+      #> snd
   in
     thy
     |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
diff -r ed431cc99f17 -r b5492f611129 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jun 14 12:01:30 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 14 12:01:30 2010 +0200
@@ -59,6 +59,9 @@
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Attrib.src
+  val add_nbe_default_eqn: thm -> theory -> theory
+  val add_nbe_default_eqn_attribute: attribute
+  val add_nbe_default_eqn_attrib: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val add_case: thm -> theory -> theory
@@ -1066,18 +1069,25 @@
    of SOME eqn => gen_add_eqn false eqn thy
     | NONE => thy;
 
+fun add_nbe_eqn thm thy =
+  gen_add_eqn false (mk_eqn thy (thm, false)) thy;
+
 fun add_default_eqn thm thy =
   case mk_eqn_liberal thy thm
    of SOME eqn => gen_add_eqn true eqn thy
     | NONE => thy;
 
-fun add_nbe_eqn thm thy =
-  gen_add_eqn false (mk_eqn thy (thm, false)) thy;
-
 val add_default_eqn_attribute = Thm.declaration_attribute
   (fn thm => Context.mapping (add_default_eqn thm) I);
 val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
 
+fun add_nbe_default_eqn thm thy =
+  gen_add_eqn true (mk_eqn thy (thm, false)) thy;
+
+val add_nbe_default_eqn_attribute = Thm.declaration_attribute
+  (fn thm => Context.mapping (add_nbe_default_eqn thm) I);
+val add_nbe_default_eqn_attrib = Attrib.internal (K add_nbe_default_eqn_attribute);
+
 fun add_abs_eqn raw_thm thy =
   let
     val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm;