src/HOL/Tools/datatype_rep_proofs.ML
changeset 11628 e57a6e51715e
parent 11539 0f17da240450
child 11806 e1fd22a657ae
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
     1.3 @@ -175,7 +175,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