src/HOL/Tools/datatype_rep_proofs.ML
changeset 12180 91c9f661b183
parent 11957 f1657e0291ca
child 12922 ed70a600f0ea
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Nov 14 18:42:34 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Nov 14 18:44:27 2001 +0100
     1.3 @@ -180,7 +180,7 @@
     1.4      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
     1.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     1.6          (InductivePackage.add_inductive_i false true big_rec_name false true false
     1.7 -           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
     1.8 +           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1;
     1.9  
    1.10      (********************************* typedef ********************************)
    1.11