--- 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;