First attaches the suffix "a" and then increments this;

   First attaches the suffix "a" and then increments this;

   preserves a suffix of underscores "_". *)

   preserves a suffix of underscores "_". *)

 fun variant bs name =

 fun variant bs name =

   let

   let

     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));

     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));

     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 (c ^ "a") else c;

   in vary1 (if c = "" then "u" else c) ^ u end;

   in vary1 (if c = "" then "u" else c) ^ u end;

 (*Create variants of the list of names, with priority to the first ones*)

 (*Create variants of the list of names, with priority to the first ones*)

 fun variantlist ([], used) = []

 fun variantlist ([], used) = []