src/HOL/Tools/datatype_rep_proofs.ML
changeset 6522 2f6cec5c046f
parent 6427 fd36b2e7d80e
child 7015 85be09eb136c
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Apr 27 10:50:31 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Apr 27 10:50:50 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 (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
+           consts [] (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
 
     (********************************* typedef ********************************)