src/HOL/Nominal/nominal_inductive2.ML

 
 fun prove_strong_ind s alt_name avoids ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive ctxt (Sign.intern_const thy s);
+      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
     val ind_params = Inductive.params_of raw_induct;
     val raw_induct = atomize_induct ctxt raw_induct;
     val elims = map (atomize_induct ctxt) elims;
     val monos = Inductive.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;