src/Tools/IsaPlanner/rw_inst.ML

     let val rep = Thm.rep_thm th
       val hyps = #hyps rep
       val (tpairl,tpairr) = Library.split_list (#tpairs rep)
       val prop = #prop rep
     in
-      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
+      List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
     end;
 
 (* Given a list of variables that were bound, and a that has been
 instantiated with free variable placeholders for the bound vars, it
 creates an abstracted version of the theorem, with local bound vars as

       other uninstantiated vars in the hyps of the rule 
       ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
 fun mk_renamings tgt rule_inst = 
     let
       val rule_conds = Thm.prems_of rule_inst
-      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
+      val names = foldr OldTerm.add_term_names [] (tgt :: rule_conds);
       val (conds_tyvs,cond_vs) = 
           Library.foldl (fn ((tyvs, vs), t) => 
                     (Library.union
-                       (Term.term_tvars t, tyvs),
+                       (OldTerm.term_tvars t, tyvs),
                      Library.union 
                        (map Term.dest_Var (OldTerm.term_vars t), vs))) 
                 (([],[]), rule_conds);
       val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
       val vars_to_fix = Library.union (termvars, cond_vs);

 fun mk_fixtvar_tyinsts ignore_insts ts = 
     let 
       val ignore_ixs = map fst ignore_insts;
       val (tvars, tfrees) = 
             foldr (fn (t, (varixs, tfrees)) => 
-                      (Term.add_term_tvars (t,varixs),
-                       Term.add_term_tfrees (t,tfrees)))
+                      (OldTerm.add_term_tvars (t,varixs),
+                       OldTerm.add_term_tfrees (t,tfrees)))
                   ([],[]) ts;
         val unfixed_tvars = 
             List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
         val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
     in (fixtyinsts, tfrees) end;