src/HOL/Tools/datatype_rep_proofs.ML
changeset 11628 e57a6e51715e
parent 11539 0f17da240450
child 11806 e1fd22a657ae
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
@@ -175,7 +175,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) [Funs_mono] []) thy1;
+           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
 
     (********************************* typedef ********************************)