replaced Term.variant(list) by Name.variant(_list);
Name.bound;

--- a/src/Pure/meta_simplifier.ML	Tue Jul 11 12:17:03 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Jul 11 12:17:04 2006 +0200
@@ -258,7 +258,7 @@
 fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
   let
     val used = Term.add_term_names (t, []);
-    val xs = rev (Term.variantlist (rev (map #2 bs), used));
+    val xs = rev (Name.variant_list used (rev (map #2 bs)));
     fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
 
@@ -964,7 +964,7 @@
        (case term_of t0 of
            Abs (a, T, t) =>
              let
-                 val b = Term.bound (#1 bounds);
+                 val b = Name.bound (#1 bounds);
                  val (v, t') = Thm.dest_abs (SOME b) t0;
                  val b' = #1 (Term.dest_Free (Thm.term_of v));
                  val _ = conditional (b <> b') (fn () =>
@@ -1148,7 +1148,7 @@
   let
     val Simpset ({bounds = (_, bounds), ...}, _) = ss;
     val bs = fold_aterms (fn Free (x, _) =>
-        if Term.is_bound x andalso not (AList.defined eq_bound bounds x)
+        if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
         then insert (op =) x else I
       | _ => I) (term_of ct) [];
   in

--- a/src/Pure/pattern.ML	Tue Jul 11 12:17:03 2006 +0200
+++ b/src/Pure/pattern.ML	Tue Jul 11 12:17:04 2006 +0200
@@ -413,7 +413,7 @@
 fun matches_subterm thy (pat,obj) =
   let fun msub(bounds,obj) = matches thy (pat,obj) orelse
             (case obj of
-              Abs(x,T,t) => let val y = variant bounds x
+              Abs(x,T,t) => let val y = Name.variant bounds x
                                 val f = Free(":" ^ y,T)
                             in msub(x::bounds,subst_bound(f,t)) end
             | s$t => msub(bounds,s) orelse msub(bounds,t)
@@ -442,7 +442,7 @@
 
     fun variant_absfree bounds (x, T, t) =
       let
-        val (x', t') = Term.dest_abs (Term.bound bounds, T, t);
+        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
         fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
       in (abs, t') end;