src/HOL/Tools/datatype_abs_proofs.ML
changeset 11628 e57a6e51715e
parent 11539 0f17da240450
child 11754 3928d990c22f
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 19:18:46 2001 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 28 19:19:26 2001 +0200
@@ -182,7 +182,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) [fun_rel_comp_mono] []) thy0;
+           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)