# HG changeset patch
# User berghofe
# Date 1035213384 -7200
# Node ID 0009325e9af013869eb9c4128b159380ea35138a
# Parent  a2730043029bfed17d1e79ee4ef3f52714dd5784
Replaced variantlist (quadratic) by gen_names (linear).

diff -r a2730043029b -r 0009325e9af0 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Oct 21 17:15:40 2002 +0200
+++ b/src/Pure/type_infer.ML	Mon Oct 21 17:16:24 2002 +0200
@@ -227,6 +227,11 @@
 
 (* typs_terms_of *)                             (*DESTRUCTIVE*)
 
+fun gen_names 0 _ _ = []
+  | gen_names i s used = if s mem used
+      then gen_names i (Symbol.bump_string s) used
+      else s :: gen_names (i-1) (Symbol.bump_string s) used;
+
 fun typs_terms_of used mk_var prfx (Ts, ts) =
   let
     fun elim (r as ref (Param S), x) = r := mk_var (x, S)
@@ -234,8 +239,7 @@
 
     val used' = foldl add_names (foldl add_namesT (used, Ts), ts);
     val parms = rev (foldl add_parms (foldl add_parmsT ([], Ts), ts));
-    val pre_names = replicate (length parms) (prfx ^ "'");
-    val names = variantlist (pre_names, prfx ^ "'" :: used');
+    val names = gen_names (length parms) (prfx ^ "'a") used';
   in
     seq2 elim (parms, names);
     (map simple_typ_of Ts, map simple_term_of ts)