moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use regular Term.add_XXX etc.;

--- a/src/Pure/Isar/locale.ML	Wed Dec 31 18:53:18 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Dec 31 18:53:19 2008 +0100
@@ -714,7 +714,7 @@
     val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
 
     fun inst_parms (i, ps) =
-      List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
+      List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps)
       |> map_filter (fn (a, S) =>
           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
           in if T = TFree (a, S) then NONE else SOME (a, T) end)
@@ -1791,10 +1791,11 @@
     val name = Sign.full_bname thy bname;
 
     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
-    val env = Term.add_term_free_names (body, []);
+    val env = Term.add_free_names body [];
     val xs = filter (member (op =) env o #1) parms;
     val Ts = map #2 xs;
-    val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
+    val extraTs =
+      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
       |> Library.sort_wrt #1 |> map TFree;
     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
 
@@ -1949,8 +1950,8 @@
     val elemss = import_elemss @ body_elemss |>
       map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
 
-    val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
-      List.foldr Term.add_typ_tfrees [] (map snd parms);
+    val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\
+      List.foldr OldTerm.add_typ_tfrees [] (map snd parms);
     val _ = if null extraTs then ()
       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
 

--- a/src/Pure/type.ML	Wed Dec 31 18:53:18 2008 +0100
+++ b/src/Pure/type.ML	Wed Dec 31 18:53:19 2008 +0100
@@ -265,9 +265,9 @@
 (* no_tvars *)
 
 fun no_tvars T =
-  (case typ_tvars T of [] => T
+  (case Term.add_tvarsT T [] of [] => T
   | vs => raise TYPE ("Illegal schematic type variable(s): " ^
-      commas_quote (map (Term.string_of_vname o #1) vs), [T], []));
+      commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
 
 
 (* varify *)
@@ -307,8 +307,8 @@
 (*this sort of code could replace unvarifyT*)
 fun freeze_thaw_type T =
   let
-    val used = add_typ_tfree_names (T, [])
-    and tvars = map #1 (add_typ_tvars (T, []));
+    val used = OldTerm.add_typ_tfree_names (T, [])
+    and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
     val (alist, _) = List.foldr new_name ([], used) tvars;
   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
 
@@ -316,8 +316,8 @@
 
 fun freeze_thaw t =
   let
-    val used = it_term_types add_typ_tfree_names (t, [])
-    and tvars = map #1 (it_term_types add_typ_tvars (t, []));
+    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
+    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
     val (alist, _) = List.foldr new_name ([], used) tvars;
   in
     (case alist of

--- a/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 18:53:18 2008 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML	Wed Dec 31 18:53:19 2008 +0100
@@ -81,7 +81,7 @@
 
 datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
 
-fun is_polymorphic (Constant (_, _, ty)) = not (null (typ_tvars ty))
+fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty []))
 
 fun distinct_constants cs =
     Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
@@ -90,7 +90,7 @@
     let
         val cs = distinct_constants (filter is_polymorphic cs)
         val old_cs = cs
-(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (typ_tvars ty) tab
+(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
         val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
         fun tvars_of ty = collect_tvars ty Typtab.empty
         val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
@@ -262,10 +262,10 @@
 let
     val (left, right) = collect_consts_of_thm th
     val polycs = filter Linker.is_polymorphic left
-    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
+    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
     fun check_const (c::cs) cs' =
         let
-            val tvars = typ_tvars (Linker.typ_of_constant c)
+            val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
             val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
         in
             if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"