--- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Feb 25 12:05:58 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Feb 25 16:31:15 2008 +0100
@@ -177,11 +177,11 @@
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;
+ (InductivePackage.add_inductive_global (serial_string ())
+ {verbose = false, kind = Thm.internalK, 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;
(********************************* typedef ********************************)