src/HOL/Tools/inductive_codegen.ML

           val cs = fold Term.add_const_names (Thm.prems_of thm) [];
           val rules = Symtab.lookup_list intros s;
           val nparms = (case optnparms of
             SOME k => k
           | NONE => (case rules of
-             [] => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
+             [] => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
                  SOME (_, {raw_induct, ...}) =>
                    length (Inductive.params_of raw_induct)
                | NONE => 0)
             | xs => snd (snd (snd (split_last xs)))))
         in CodegenData.put

   end) I);
 
 fun get_clauses thy s =
   let val {intros, graph, ...} = CodegenData.get thy
   in case Symtab.lookup intros s of
-      NONE => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
+      NONE => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
         NONE => NONE
       | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
           SOME (names, Codegen.thyname_of_const thy s,
             length (Inductive.params_of raw_induct),
             preprocess thy intrs))