eliminated some legacy operations;

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 13:59:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 14:26:43 2011 +0100
@@ -83,8 +83,7 @@
       else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
     val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
     val unneeded_vars =
-      subtract (op =)
-        (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+      subtract (op =) (fold Term.add_tfree_namesT (leafTs' @ branchTs) []) (hd tyvars);
     val leafTs =
       leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
@@ -386,7 +385,7 @@
         val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
-        val used = Misc_Legacy.add_term_tfree_names (a, []);
+        val used = Term.add_tfree_names a [];
 
         fun mk_thm i =
           let
@@ -708,7 +707,7 @@
           let
             val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
             val _ =
-              (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
+              (case subtract (op =) tvs (fold Term.add_tfree_namesT cargs' []) of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs));
             val c = Sign.full_name_path tmp_thy (Binding.name_of tname) cname;

--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 02 13:59:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 02 14:26:43 2011 +0100
@@ -95,7 +95,7 @@
 
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
-    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
 
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
@@ -292,7 +292,7 @@
 
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
-    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
 

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 02 13:59:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 02 14:26:43 2011 +0100
@@ -139,12 +139,12 @@
       else pair NONE;
     val flt =
       if null indnames then I
-      else filter (fn Free (s, _) => member (op =) indnames s | _ => false);
+      else filter (member (op =) indnames o fst);
     fun abstr (t1, t2) =
       (case t1 of
         NONE =>
-          (case flt (Misc_Legacy.term_frees t2) of
-            [Free (s, T)] => SOME (absfree (s, T) t2)
+          (case flt (Term.add_frees t2 []) of
+            [(s, T)] => SOME (absfree (s, T) t2)
           | _ => NONE)
       | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))));
     val insts =

--- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Dec 02 13:59:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Dec 02 14:26:43 2011 +0100
@@ -371,9 +371,9 @@
 fun strip_case'' dest (pat, rhs) =
   (case dest (Term.add_free_names pat []) rhs of
     SOME (exp as Free _, clauses) =>
-      if member op aconv (Misc_Legacy.term_frees pat) exp andalso
+      if Term.exists_subterm (curry (op aconv) exp) pat andalso
         not (exists (fn (_, rhs') =>
-          member op aconv (Misc_Legacy.term_frees rhs') exp) clauses)
+          Term.exists_subterm (curry (op aconv) exp) rhs') clauses)
       then
         maps (strip_case'' dest) (map (fn (pat', rhs') =>
           (subst_free [(exp, pat')] pat, rhs')) clauses)

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 02 13:59:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 02 14:26:43 2011 +0100
@@ -406,7 +406,7 @@
         Syntax.string_of_typ ctxt T);
     fun type_of_constr (cT as (_, T)) =
       let
-        val frees = Misc_Legacy.typ_tfrees T;
+        val frees = Term.add_tfreesT T [];
         val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
           handle TYPE _ => no_constr cT
         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();

--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Dec 02 13:59:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Dec 02 14:26:43 2011 +0100
@@ -217,7 +217,7 @@
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
-    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used = fold Term.add_tfree_namesT recTs [];
 
     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
 
@@ -269,7 +269,7 @@
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
-    val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
 
@@ -316,7 +316,7 @@
   let
     val descr' = flat descr;
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
-    val used' = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
+    val used' = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);