# HG changeset patch
# User wenzelm
# Date 1257450282 -3600
# Node ID 4da71b27b3fedb1ac923878cefa3ce65a3e9efd4
# Parent  485fd398dd33b7a803984ce19b23831b9003b120
declare Spec_Rules for most basic definitional packages;

diff -r 485fd398dd33 -r 4da71b27b3fe src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Thu Nov 05 20:41:45 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Thu Nov 05 20:44:42 2009 +0100
@@ -44,7 +44,8 @@
           else ());
     val b = Binding.name c;
 
-    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
+    val head = Const (Sign.full_bname thy c, T);
+    val def = Term.subst_atomic [(Free (c, T), head)] prop;
     val name = Thm.def_binding_optional b raw_name;
     val atts = map (prep_att thy) raw_atts;
 
@@ -52,7 +53,10 @@
       thy
       |> Sign.add_consts_i [(b, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
-      |-> (fn [thm] => Code.add_default_eqn thm #> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
+      |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
+        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
+        Code.add_default_eqn thm #>
+        Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
   in ((c, T), thy') end;
 
 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
diff -r 485fd398dd33 -r 4da71b27b3fe src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Nov 05 20:41:45 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 05 20:44:42 2009 +0100
@@ -201,19 +201,23 @@
                 Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val name = Thm.def_binding_optional b raw_name;
-    val ((lhs, (_, th)), lthy2) = lthy
+    val ((lhs, (_, raw_th)), lthy2) = lthy
       |> LocalTheory.define Thm.definitionK
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
-    val ((def_name, [th']), lthy3) = lthy2
+
+    val th = prove lthy2 raw_th;
+    val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
+
+    val ((def_name, [th']), lthy4) = lthy3
       |> LocalTheory.note Thm.definitionK
-        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: Code.add_default_eqn_attrib :: atts),
-          [prove lthy2 th]);
+        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
+            Code.add_default_eqn_attrib :: atts), [th]);
 
-    val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
+    val lhs' = Morphism.term (LocalTheory.target_morphism lthy4) lhs;
     val _ =
       if not do_print then ()
-      else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
-  in ((lhs, (def_name, th')), lthy3) end;
+      else print_consts lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+  in ((lhs, (def_name, th')), lthy4) end;
 
 val definition = gen_def false check_free_spec;
 val definition_cmd = gen_def true read_free_spec;