--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Oct 02 19:05:20 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Oct 02 22:23:24 2007 +0200
@@ -155,7 +155,8 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
setmp InductivePackage.quiet_mode (!quiet_mode)
- (InductivePackage.add_inductive_global false big_rec_name' false false true
+ (InductivePackage.add_inductive_global {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;