# HG changeset patch
# User wenzelm
# Date 1006904373 -3600
# Node ID 749a04f0cfb0efe5e60cda6e67c476fd6838615d
# Parent  3c3f98b3d9e70672ee6ccf8040bdedabfe673eac
variant: preserve suffix of underscores (for skolem/internal names etc.);

diff -r 3c3f98b3d9e7 -r 749a04f0cfb0 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Nov 28 00:38:11 2001 +0100
+++ b/src/Pure/term.ML	Wed Nov 28 00:39:33 2001 +0100
@@ -726,13 +726,15 @@
 
 (*** Printing ***)
 
-
 (*Makes a variant of the name c distinct from the names in bs.
-  First attaches the suffix "a" and then increments this. *)
-fun variant bs c : string =
-  let fun vary2 c = if (c mem_string bs) then  vary2 (bump_string c)  else  c
-      fun vary1 c = if (c mem_string bs) then  vary2 (c ^ "a")  else  c
-  in  vary1 (if c="" then "u" else c)  end;
+  First attaches the suffix "a" 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 (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;
 
 (*Create variants of the list of names, with priority to the first ones*)
 fun variantlist ([], used) = []