eliminated some legacy operations;

--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:54:25 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 15:23:27 2011 +0100
@@ -1414,7 +1414,7 @@
 
     val _ = warning "defining recursion combinator ...";
 
-    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used = fold Term.add_tfree_namesT recTs [];
 
     val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
 

--- a/src/HOL/Statespace/state_space.ML	Fri Dec 02 14:54:25 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Dec 02 15:23:27 2011 +0100
@@ -470,7 +470,7 @@
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     val T = Syntax.read_typ ctxt' raw_T;
-    val env' = Misc_Legacy.add_typ_tfrees (T, env);
+    val env' = Term.add_tfreesT T env;
   in (T, env') end;
 
 fun cert_typ ctxt raw_T env =
@@ -478,7 +478,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val T = Type.no_tvars (Sign.certify_typ thy raw_T)
       handle TYPE (msg, _, _) => error msg;
-    val env' = Misc_Legacy.add_typ_tfrees (T, env);
+    val env' = Term.add_tfreesT T env;
   in (T, env') end;
 
 fun gen_define_statespace prep_typ state_space args name parents comps thy =

--- a/src/HOL/Tools/record.ML	Fri Dec 02 14:54:25 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 02 15:23:27 2011 +0100
@@ -1495,7 +1495,7 @@
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     val T = Syntax.read_typ ctxt' raw_T;
-    val env' = Misc_Legacy.add_typ_tfrees (T, env);
+    val env' = Term.add_tfreesT T env;
   in (T, env') end;
 
 fun cert_typ ctxt raw_T env =
@@ -1503,7 +1503,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val T = Type.no_tvars (Sign.certify_typ thy raw_T)
       handle TYPE (msg, _, _) => error msg;
-    val env' = Misc_Legacy.add_typ_tfrees (T, env);
+    val env' = Term.add_tfreesT T env;
   in (T, env') end;
 
 

--- a/src/HOL/Tools/refute.ML	Fri Dec 02 14:54:25 2011 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Dec 02 15:23:27 2011 +0100
@@ -403,8 +403,7 @@
 
 fun close_form t =
   let
-    (* (Term.indexname * Term.typ) list *)
-    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
+    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
   in
     fold (fn ((x, i), T) => fn t' =>
       Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
@@ -1212,8 +1211,7 @@
       error "Term to be refuted contains schematic type variables"
 
     (* existential closure over schematic variables *)
-    (* (Term.indexname * Term.typ) list *)
-    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
+    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
     (* Term.term *)
     val ex_closure = fold (fn ((x, i), T) => fn t' =>
       HOLogic.exists_const T $