# HG changeset patch # User wenzelm # Date 924093643 -7200 # Node ID 965705537d5b306f10e6e823290f25595426f653 # Parent 037f3446e9e5e9a465f07552c8d8d314d0e16e62 intrs: provide names and atts; diff -r 037f3446e9e5 -r 965705537d5b src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 14 11:32:50 1999 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Apr 14 14:40:43 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 rec_intr_ts [] []) thy0; + rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0; (* prove uniqueness and termination of primrec combinators *) diff -r 037f3446e9e5 -r 965705537d5b src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 14 11:32:50 1999 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 14 14:40:43 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 intr_ts [] []) thy1; + consts (map (fn x => (("", x), [])) intr_ts) [] []) thy1; (********************************* typedef ********************************)