src/HOL/Tools/datatype_abs_proofs.ML

         (([], 0), descr' ~~ recTs ~~ rec_sets);
 
     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 *)
 
     val _ = message "Proving termination and uniqueness of primrec functions ...";