src/HOL/Import/proof_kernel.ML

     let
       fun ERR s = error ("Drule.disambiguate_frees: "^s)
       val ct = cprop_of thm
       val t = term_of ct
       val thy = theory_of_cterm ct
-      val frees = OldTerm.term_frees t
+      val frees = Misc_Legacy.term_frees t
       val freenames = Term.add_free_names t []
       val is_old_name = member (op =) freenames
       fun name_of (Free (n, _)) = n
         | name_of _ = ERR "name_of"
       fun new_name' bump map n =

 
 fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy =
     let
         val _ = message "INST_TYPE:"
         val _ = if_debug pth hth
-        val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
+        val tys_before = Misc_Legacy.add_term_tfrees (prop_of th,[])
         val th1 = Thm.varifyT_global th
-        val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
+        val tys_after = Misc_Legacy.add_term_tvars (prop_of th1,[])
         val tyinst = map (fn (bef, iS) =>
                              (case try (Lib.assoc (TFree bef)) lambda of
                                   SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
                                 | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
                              ))

             val (HOLThm(rens,td_th)) = norm_hthm thy hth
             val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
             val c = case concl_of th2 of
                         _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "new_type_definition" "Bad type definition theorem"
-            val tfrees = OldTerm.term_tfrees c
+            val tfrees = Misc_Legacy.term_tfrees c
             val tnames = map fst tfrees
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
               Typedef.add_typedef_global false (SOME (Binding.name thmname))

                                     SOME (cterm_of thy t)] light_nonempty
             val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
             val c = case concl_of th2 of
                         _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
                       | _ => raise ERR "type_introduction" "Bad type definition theorem"
-            val tfrees = OldTerm.term_tfrees c
+            val tfrees = Misc_Legacy.term_tfrees c
             val tnames = sort_strings (map fst tfrees)
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
               Typedef.add_typedef_global false NONE