# HG changeset patch
# User wenzelm
# Date 1201363715 -3600
# Node ID b0604cd8e5e104febe158791028e989d085fcb7b
# Parent  11c6811f232c3a8c5779c207e96121a333ab05ed
internal inductive: fresh theorem group;

diff -r 11c6811f232c -r b0604cd8e5e1 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Jan 25 23:50:33 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Jan 26 17:08:35 2008 +0100
@@ -564,6 +564,7 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       setmp InductivePackage.quiet_mode false
         (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            group = serial_string (),  (* FIXME pass proper group (!?) *)
             alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
            (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
               (rep_set_names' ~~ recTs'))
@@ -1488,6 +1489,7 @@
       thy10 |>
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            group = serial_string (),  (* FIXME pass proper group (!?) *)
             alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map dest_Free rec_fns)
diff -r 11c6811f232c -r b0604cd8e5e1 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jan 25 23:50:33 2008 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jan 26 17:08:35 2008 +0100
@@ -156,6 +156,7 @@
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            group = serial_string (),  (* FIXME pass proper group (!?) *)
             alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true}
            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map dest_Free rec_fns)
diff -r 11c6811f232c -r b0604cd8e5e1 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jan 25 23:50:33 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jan 26 17:08:35 2008 +0100
@@ -178,6 +178,7 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       setmp InductivePackage.quiet_mode (! quiet_mode)
         (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            group = serial_string (),  (* FIXME pass proper group (!?) *)
             alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false}
            (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) []) thy1;
diff -r 11c6811f232c -r b0604cd8e5e1 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Jan 25 23:50:33 2008 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Jan 26 17:08:35 2008 +0100
@@ -43,6 +43,7 @@
           InductivePackage.add_inductive_i
             {verbose = ! Toplevel.debug,
               kind = Thm.internalK,
+              group = serial_string (),   (* FIXME pass proper group (!?) *)
               alt_name = "",
               coind = false,
               no_elim = false,
diff -r 11c6811f232c -r b0604cd8e5e1 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jan 25 23:50:33 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 26 17:08:35 2008 +0100
@@ -351,6 +351,7 @@
 
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
+          group = serial_string (),  (* FIXME pass proper group (!?) *)
           alt_name = "", coind = false, no_elim = false, no_ind = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Sign.base_name (name_of_thm intr), []),