--- a/src/HOL/Nominal/nominal_inductive.ML Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Jan 01 14:23:39 2009 +0100
@@ -152,7 +152,7 @@
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));