src/HOL/Tools/datatype_rep_proofs.ML
changeset 12180 91c9f661b183
parent 11957 f1657e0291ca
child 12922 ed70a600f0ea
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Nov 14 18:42:34 2001 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Nov 14 18:44:27 2001 +0100
@@ -180,7 +180,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 ********************************)