src/HOL/Import/proof_kernel.ML

       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 freenames = add_term_free_names (t, [])
+      val freenames = OldTerm.add_term_free_names (t, [])
       fun is_old_name n = n mem_string freenames
       fun name_of (Free (n, _)) = n
         | name_of _ = ERR "name_of"
       fun new_name' bump map n =
           let val n' = n^bump in

 fun non_trivial_term_consts tm =
     List.filter (fn c => not (c = "Trueprop" orelse
                          c = "All" orelse
                          c = "op -->" orelse
                          c = "op &" orelse
-                         c = "op =")) (Term.term_consts tm)
+                         c = "op =")) (OldTerm.term_consts tm)
 
 fun match_consts t (* th *) =
     let
         fun add_consts (Const (c, _), cs) =
             (case c of

 
 fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy =
     let
         val _ = message "INST_TYPE:"
         val _ = if_debug pth hth
-        val tys_before = add_term_tfrees (prop_of th,[])
+        val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
         val th1 = Thm.varifyT th
-        val tys_after = add_term_tvars (prop_of th1,[])
+        val tys_after = OldTerm.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("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
                       | _ => raise ERR "new_type_definition" "Bad type definition theorem"
-            val tfrees = term_tfrees c
+            val tfrees = OldTerm.term_tfrees c
             val tnames = map fst tfrees
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2

                                     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("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
                       | _ => raise ERR "type_introduction" "Bad type definition theorem"
-            val tfrees = term_tfrees c
+            val tfrees = OldTerm.term_tfrees c
             val tnames = sort string_ord (map fst tfrees)
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2