src/HOL/Nominal/nominal_inductive.ML

     val ind_params = InductivePackage.params_of raw_induct;
     val raw_induct = atomize_induct ctxt raw_induct;
     val elims = map (atomize_induct ctxt) elims;
     val monos = InductivePackage.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
-    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
+    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
     val induct_cases = map fst (fst (RuleCases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));