--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Dec 31 18:53:16 2008 +0100
@@ -158,7 +158,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 #> add_term_consts) [] eqvt_thms of
+ val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
@@ -221,8 +221,8 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Sign.base_name a)) atoms);
- val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n";
- val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z";
+ val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
+ val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
val fsT = TFree (fs_ctxt_tyname, ind_sort);
val inductive_forall_def' = Drule.instantiate'