src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

         if is_some (try (map (cterm_of thy)) intr_ts) then
           let
             val (ind_result, thy') =
               thy
               |> Sign.map_naming Name_Space.conceal
-              |> Inductive.add_inductive_global (serial ())
+              |> Inductive.add_inductive_global
                 {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
                   no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
                 (map (fn (s, T) =>
                   ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
                 pnames