src/HOL/Tools/Datatype/datatype.ML

     val branchTs = Datatype_Aux.get_branching_types descr' sorts;
     val branchT = if null branchTs then HOLogic.unitT
       else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
     val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
     val unneeded_vars =
-      subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+      subtract (op =) (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
     val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val (newTs, oldTs) = chop (length (hd descr)) recTs;
     val sumT = if null leafTs then HOLogic.unitT
       else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;

     fun mk_funs_inv thy thm =
       let
         val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
-        val used = OldTerm.add_term_tfree_names (a, []);
+        val used = Misc_Legacy.add_term_tfree_names (a, []);
 
         fun mk_thm i =
           let
             val Ts = map (TFree o rpair HOLogic.typeS)
               (Name.variant_list used (replicate i "'t"));

       let
         fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
           let
             val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
             val _ =
-              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
+              (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs));
             val c = Sign.full_name_path tmp_thy tname' cname;
           in
             (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],