src/HOL/Tools/datatype_rep_proofs.ML
changeset 6422 965705537d5b
parent 6394 3d9fd50fcc43
child 6427 fd36b2e7d80e
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Apr 14 11:32:50 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Apr 14 14:40:43 1999 +0200
     1.3 @@ -136,7 +136,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 intr_ts [] []) thy1;
     1.8 +           consts (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
     1.9  
    1.10      (********************************* typedef ********************************)
    1.11