--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 14 11:32:50 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 14 14:40:43 1999 +0200
@@ -136,7 +136,7 @@
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
(InductivePackage.add_inductive_i false true big_rec_name false true false
- consts intr_ts [] []) thy1;
+ consts (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
(********************************* typedef ********************************)