Term.declare_term_names;

--- a/src/Pure/Syntax/syn_trans.ML	Tue Jul 18 17:10:22 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Jul 18 20:01:41 2006 +0200
@@ -383,9 +383,9 @@
 
 (* dependent / nondependent quantifiers *)
 
-fun variant_abs' (x, T, B) =
-  let val x' = Name.variant (add_term_names (B, [])) x in
-    (x', subst_bound (mark_boundT (x', T), B))
+fun variant_abs' (x, T, b) =
+  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context) in
+    (x', subst_bound (mark_boundT (x', T), b))
   end;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =

--- a/src/Pure/meta_simplifier.ML	Tue Jul 18 17:10:22 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Jul 18 20:01:41 2006 +0200
@@ -257,8 +257,8 @@
 
 fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
   let
-    val used = Term.add_term_names (t, []);
-    val xs = rev (Name.variant_list used (rev (map #2 bs)));
+    val names = Term.declare_term_names t Name.context;
+    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
     fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;