--- 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)
--- 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)
--- 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;
--- 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,
--- 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), []),