Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adapted add_inductive;
authorwenzelm
Tue, 27 Apr 1999 10:50:50 +0200
changeset 6522 2f6cec5c046f
parent 6521 16c425fc00cb
child 6523 c84935821ba0
adapted add_inductive;
src/HOL/Tools/datatype_abs_proofs.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/datatype_rep_proofs.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Apr 27 10:50:31 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Apr 27 10:50:50 1999 +0200
@@ -170,7 +170,7 @@
     val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name' false false true
-           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
+           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Apr 27 10:50:31 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Apr 27 10:50:50 1999 +0200
@@ -136,7 +136,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) [] []) thy1;
+           consts [] (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
 
     (********************************* typedef ********************************)
isabelle