src/HOL/Tools/datatype_rep_proofs.ML

       map (make_intr rep_set_name (length constrs))
         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'));
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       setmp InductivePackage.quiet_mode (! quiet_mode)
-        (InductivePackage.add_inductive_global false big_rec_name false true false
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false}
            (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) []) thy1;
 
     (********************************* typedef ********************************)