src/HOL/Nominal/nominal_fresh_fun.ML

    fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
 (* rebuild de bruijn indices *)
    val bvs = map_index (Bound o fst) ps;
 (* select variables of the right class *)
    val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
-     (OldTerm.term_frees goal @ bvs);
+     (Misc_Legacy.term_frees goal @ bvs);
 (* build the tuple *)
    val s = (Library.foldr1 (fn (v, s) =>
        HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs)
      handle TERM _ => HOLogic.unit;
    val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename;
    val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
 (* find the variable we want to instantiate *)
-   val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
+   val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
  in
    (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    rtac fs_name_thm 1 THEN
    etac exE 1) thm
   handle Empty  => all_tac thm (* if we collected no variables then we do nothing *)

     val ss = global_simpset_of thy;
     val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
     val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
     val ss' = ss addsimps fresh_prod::abs_fresh;
     val ss'' = ss' addsimps fresh_perm_app;
-    val x = hd (tl (OldTerm.term_vars (prop_of exI)));
+    val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
     val goal = nth (prems_of thm) (i-1);
     val atom_name_opt = get_inner_fresh_fun goal;
     val n = length (Logic.strip_params goal);
     (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
     (* is the last one in the list, the inner one *)

   let
     val atom_basename = Long_Name.base_name atom_name;
     val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
     val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
     fun inst_fresh vars params i st =
-   let val vars' = OldTerm.term_vars (prop_of st);
+   let val vars' = Misc_Legacy.term_vars (prop_of st);
        val thy = theory_of_thm st;
    in case subtract (op =) vars vars' of
      [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
     | _ => error "fresh_fun_simp: Too many variables, please report."
   end
   in
   ((fn st =>
   let
-    val vars = OldTerm.term_vars (prop_of st);
+    val vars = Misc_Legacy.term_vars (prop_of st);
     val params = Logic.strip_params (nth (prems_of st) (i-1))
     (* The tactics which solve the subgoals generated
        by the conditionnal rewrite rule. *)
     val post_rewrite_tacs =
           [rtac pt_name_inst,