adapted add_inductive;
authorwenzelm
Tue Apr 27 10:50:50 1999 +0200 (1999-04-27)
changeset 65222f6cec5c046f
parent 6521 16c425fc00cb
child 6523 c84935821ba0
adapted add_inductive;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Apr 27 10:50:31 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Apr 27 10:50:50 1999 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
     1.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     1.6          (InductivePackage.add_inductive_i false true big_rec_name' false false true
     1.7 -           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
     1.8 +           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
     1.9  
    1.10      (* prove uniqueness and termination of primrec combinators *)
    1.11  
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Apr 27 10:50:31 1999 +0200
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Apr 27 10:50:50 1999 +0200
     2.3 @@ -136,7 +136,7 @@
     2.4      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
     2.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     2.6          (InductivePackage.add_inductive_i false true big_rec_name false true false
     2.7 -           consts (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
     2.8 +           consts [] (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
     2.9  
    2.10      (********************************* typedef ********************************)
    2.11