--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 14 11:32:50 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 14 14:40:43 1999 +0200
@@ -170,7 +170,7 @@
val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
(InductivePackage.add_inductive_i false true big_rec_name' false false true
- rec_sets rec_intr_ts [] []) thy0;
+ rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
(* prove uniqueness and termination of primrec combinators *)