Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
variant: use Symbol.bump_init;
authorwenzelm
Mon, 26 Apr 2004 14:58:03 +0200
changeset 14676 82721f31de3e
parent 14675 08b9c690f9cf
child 14677 33a37f091dc5
variant: use Symbol.bump_init;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- 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*)
isabelle