Replaced variantlist (quadratic) by gen_names (linear).
authorberghofe
Mon Oct 21 17:16:24 2002 +0200 (2002-10-21)
changeset 136670009325e9af0
parent 13666 a2730043029b
child 13668 11397ea8b438
Replaced variantlist (quadratic) by gen_names (linear).
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Oct 21 17:15:40 2002 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Oct 21 17:16:24 2002 +0200
     1.3 @@ -227,6 +227,11 @@
     1.4  
     1.5  (* typs_terms_of *)                             (*DESTRUCTIVE*)
     1.6  
     1.7 +fun gen_names 0 _ _ = []
     1.8 +  | gen_names i s used = if s mem used
     1.9 +      then gen_names i (Symbol.bump_string s) used
    1.10 +      else s :: gen_names (i-1) (Symbol.bump_string s) used;
    1.11 +
    1.12  fun typs_terms_of used mk_var prfx (Ts, ts) =
    1.13    let
    1.14      fun elim (r as ref (Param S), x) = r := mk_var (x, S)
    1.15 @@ -234,8 +239,7 @@
    1.16  
    1.17      val used' = foldl add_names (foldl add_namesT (used, Ts), ts);
    1.18      val parms = rev (foldl add_parms (foldl add_parmsT ([], Ts), ts));
    1.19 -    val pre_names = replicate (length parms) (prfx ^ "'");
    1.20 -    val names = variantlist (pre_names, prfx ^ "'" :: used');
    1.21 +    val names = gen_names (length parms) (prfx ^ "'a") used';
    1.22    in
    1.23      seq2 elim (parms, names);
    1.24      (map simple_typ_of Ts, map simple_term_of ts)