src/HOL/Nominal/nominal_inductive.ML

     val ctxt = ProofContext.init thy;
     val ({names, ...}, {raw_induct, ...}) =
       InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
     val raw_induct = atomize_induct raw_induct;
     val monos = InductivePackage.get_monos ctxt;
-    val eqvt_thms = NominalThmDecls.get_eqvt_thms thy;
+    val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
     val induct_cases = map fst (fst (RuleCases.get (the

            | xs => error ("No such atoms: " ^ commas xs);
          atoms)
       end;
     val perm_pi_simp = PureThy.get_thms thy (Name "perm_pi_simp");
     val eqvt_ss = HOL_basic_ss addsimps
-      (NominalThmDecls.get_eqvt_thms thy @ perm_pi_simp) addsimprocs
+      (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
       [mk_perm_bool_simproc names];
     val t = Logic.unvarify (concl_of raw_induct);
     val pi = Name.variant (add_term_names (t, [])) "pi";
     val ps = map (fst o HOLogic.dest_imp)
       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));