src/HOL/Nominal/nominal_package.ML

                 (descr ~~ rep_set_names))));
     val rep_set_names'' = map (Sign.full_name thy3) rep_set_names';
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       setmp InductivePackage.quiet_mode false
-        (InductivePackage.add_inductive_global false big_rep_name false true false
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
            (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
               (rep_set_names' ~~ recTs'))
            [] (map (fn x => (("", []), x)) intr_ts) []) thy3;
 
     (**** Prove that representing set is closed under permutation ****)

           (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets');
 
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10 |>
       setmp InductivePackage.quiet_mode (!quiet_mode)
-        (InductivePackage.add_inductive_global false big_rec_name false false false
+        (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
+            alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map dest_Free rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) []) ||>
       PureThy.hide_thms true [NameSpace.append
         (Sign.full_name thy10 big_rec_name) "induct"];