diff -r 4570584fbda9 -r a23dc0b7566f src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Feb 19 23:49:49 2002 +0100
+++ b/src/Pure/term.ML	Wed Feb 20 00:53:53 2002 +0100
@@ -738,7 +738,7 @@
 fun variant bs name =
   let
     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
-    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (bump_string c) else c;
+    fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
     fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c;
   in vary1 (if c = "" then "u" else c) ^ u end;