# HG changeset patch
# User bulwahn
# Date 1268392471 -3600
# Node ID c2884bec546367a84893ee94a0cf89419609c666
# Parent  cfde251d03a53c55c606cd89dc47b18358779616
adding Spec_Rules to definitional package inductive and inductive_set

diff -r cfde251d03a5 -r c2884bec5463 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Mar 12 12:14:30 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Mar 12 12:14:31 2010 +0100
@@ -71,7 +71,7 @@
     term list -> (Attrib.binding * term) list -> thm list ->
     term list -> (binding * mixfix) list ->
     local_theory -> inductive_result * local_theory
-  val declare_rules: binding -> bool -> bool -> string list ->
+  val declare_rules: binding -> bool -> bool -> string list -> term list ->
     thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
     thm -> local_theory -> thm list * thm list * thm * thm list * local_theory
   val add_ind_def: add_ind_def
@@ -698,7 +698,7 @@
   end;
 
 fun declare_rules rec_binding coind no_ind cnames
-    intrs intr_bindings intr_atts elims raw_induct lthy =
+    preds intrs intr_bindings intr_atts elims raw_induct lthy =
   let
     val rec_name = Binding.name_of rec_binding;
     fun rec_qualified qualified = Binding.qualify qualified rec_name;
@@ -715,6 +715,8 @@
 
     val (intrs', lthy1) =
       lthy |>
+      Spec_Rules.add
+        (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |>
       Local_Theory.notes
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th],
@@ -797,7 +799,7 @@
            rec_preds_defs lthy1);
 
     val (intrs', elims', induct, inducts, lthy2) = declare_rules rec_name coind no_ind
-      cnames intrs intr_names intr_atts elims raw_induct lthy1;
+      cnames preds intrs intr_names intr_atts elims raw_induct lthy1;
 
     val result =
       {preds = preds,
diff -r cfde251d03a5 -r c2884bec5463 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Mar 12 12:14:30 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Mar 12 12:14:31 2010 +0100
@@ -521,7 +521,7 @@
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
     val (intrs', elims', induct, inducts, lthy4) =
-      Inductive.declare_rules rec_name coind no_ind cnames
+      Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
         (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
         (map (fn th => (to_set [] (Context.Proof lthy3) th,
            map fst (fst (Rule_Cases.get th)),