diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Nominal/nominal_inductive2.ML
--- 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'