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