src/Pure/type_infer.ML
changeset 14695 9c78044b99c3
parent 13667 0009325e9af0
child 14788 9776f0c747c8
     1.1 --- a/src/Pure/type_infer.ML	Sat May 01 22:07:16 2004 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sat May 01 22:08:57 2004 +0200
     1.3 @@ -227,11 +227,6 @@
     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 @@ -239,7 +234,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 names = gen_names (length parms) (prfx ^ "'a") used';
    1.20 +    val names = Term.invent_names used' (prfx ^ "'a") (length parms);
    1.21    in
    1.22      seq2 elim (parms, names);
    1.23      (map simple_typ_of Ts, map simple_term_of ts)