--- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Feb 25 12:05:58 2008 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Feb 25 16:31:15 2008 +0100
@@ -155,12 +155,12 @@
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)
- (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
+ (InductivePackage.add_inductive_global (serial_string ())
+ {verbose = false, kind = Thm.internalK, 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)
+ (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
(* prove uniqueness and termination of primrec combinators *)