src/HOL/Nominal/nominal_inductive2.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 #> 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));
     val induct_cases = map fst (fst (RuleCases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));

     val atomTs = distinct op = (maps (map snd o #2) prems);
     val atoms = map (fst o dest_Type) atomTs;
     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'
       [SOME (ctyp_of thy fsT)] [] inductive_forall_def;