src/HOL/Tools/inductive.ML

 
 fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> Named_Target.init NONE
+      |> Named_Target.theory_init
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);
   in (info, ProofContext.theory_of ctxt') end;