--- 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;