# HG changeset patch
# User haftmann
# Date 1135274895 -3600
# Node ID 00190b1fa5b378e2d0d5760b0f53d7b23dd08dcf
# Parent  343da052b961f4a433de37c859668d69aecc4bbf
slight improvements

diff -r 343da052b961 -r 00190b1fa5b3 src/Pure/General/name_mangler.ML
--- a/src/Pure/General/name_mangler.ML	Thu Dec 22 17:57:09 2005 +0100
+++ b/src/Pure/General/name_mangler.ML	Thu Dec 22 19:08:15 2005 +0100
@@ -60,14 +60,20 @@
 fun mk_unique_multi eq mk seeds used =
   let
     fun mk_names i =
-      let
-        val names = map (fn seed => mk (seed, i)) seeds
-      in
-        if null (gen_inter eq (used, names))
-        then names
-        else mk_names (i+1)
-      end;
-    val names = mk_names 0;
+      if i < 2 then
+        let
+          val names = map (fn seed => mk (seed, i)) seeds
+        in
+          if null (gen_inter eq (used, names))
+            andalso (not oo has_duplicates) eq names
+          then names
+          else mk_names (i+1)
+        end
+      else
+        used
+        |> fold_map (mk_unique eq mk) seeds
+        |> fst;
+      val names = mk_names 0;
   in (names, fold cons names used) end;
 
 val empty = (Srctab.empty, Symtab.empty);