# HG changeset patch
# User wenzelm
# Date 1082984283 -7200
# Node ID 82721f31de3ef565e22d961f4c61580b6e8e5223
# Parent  08b9c690f9cf1241dd423bfd5b00cba0bd4bf998
variant: use Symbol.bump_init;

diff -r 08b9c690f9cf -r 82721f31de3e src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Apr 26 14:57:30 2004 +0200
+++ b/src/Pure/term.ML	Mon Apr 26 14:58:03 2004 +0200
@@ -757,14 +757,14 @@
 
 (*** Printing ***)
 
-(*Makes a variant of the name c distinct from the names in bs.
-  First attaches the suffix "a" and then increments this;
+(*Makes a variant of a name distinct from the names in bs.
+  First attaches the suffix and then increments this;
   preserves a suffix of underscores "_". *)
 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 (Symbol.bump_string c) else c;
-    fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c;
+    fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c;
   in vary1 (if c = "" then "u" else c) ^ u end;
 
 (*Create variants of the list of names, with priority to the first ones*)