improved Term.invent_names;
authorwenzelm
Sat May 01 22:08:57 2004 +0200 (2004-05-01 ago)
changeset 146959c78044b99c3
parent 14694 49873d345a39
child 14696 e862cc138e9c
improved Term.invent_names;
src/Pure/Isar/locale.ML
src/Pure/axclass.ML
src/Pure/term.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Sat May 01 22:07:16 2004 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Sat May 01 22:08:57 2004 +0200
     1.3 @@ -476,7 +476,7 @@
     1.4    let
     1.5      val tvars = rev (foldl Term.add_tvarsT ([], Ts));
     1.6      val tfrees = map TFree
     1.7 -      (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars);
     1.8 +      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
     1.9    in map #1 tvars ~~ tfrees end;
    1.10  
    1.11  fun unify_frozen ctxt maxidx Ts Us =
     2.1 --- a/src/Pure/axclass.ML	Sat May 01 22:07:16 2004 +0200
     2.2 +++ b/src/Pure/axclass.ML	Sat May 01 22:08:57 2004 +0200
     2.3 @@ -96,7 +96,7 @@
     2.4  
     2.5  fun mk_arity (t, Ss, c) =
     2.6    let
     2.7 -    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length Ss), Ss);
     2.8 +    val tfrees = ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss);
     2.9    in Logic.mk_inclass (Type (t, tfrees), c) end;
    2.10  
    2.11  fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S;
     3.1 --- a/src/Pure/term.ML	Sat May 01 22:07:16 2004 +0200
     3.2 +++ b/src/Pure/term.ML	Sat May 01 22:08:57 2004 +0200
     3.3 @@ -181,7 +181,6 @@
     3.4    val match_bvars: (term * term) * (string * string) list -> (string * string) list
     3.5    val rename_abs: term -> term -> term -> term option
     3.6    val invent_names: string list -> string -> int -> string list
     3.7 -  val invent_type_names: string list -> int -> string list
     3.8    val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
     3.9    val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
    3.10    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    3.11 @@ -773,8 +772,13 @@
    3.12        let val b' = variant used b
    3.13        in  b' :: variantlist (bs, b'::used)  end;
    3.14  
    3.15 -fun invent_names used prfx n = variantlist (Library.replicate n prfx, prfx :: used);
    3.16 -fun invent_type_names used = invent_names used "'";
    3.17 +(*Invent fresh names*)
    3.18 +fun invent_names _ _ 0 = []
    3.19 +  | invent_names used a n =
    3.20 +      let val b = Symbol.bump_string a in
    3.21 +        if a mem_string used then invent_names used b n
    3.22 +        else a :: invent_names used b (n - 1)
    3.23 +      end;
    3.24  
    3.25  
    3.26  
     4.1 --- a/src/Pure/type_infer.ML	Sat May 01 22:07:16 2004 +0200
     4.2 +++ b/src/Pure/type_infer.ML	Sat May 01 22:08:57 2004 +0200
     4.3 @@ -227,11 +227,6 @@
     4.4  
     4.5  (* typs_terms_of *)                             (*DESTRUCTIVE*)
     4.6  
     4.7 -fun gen_names 0 _ _ = []
     4.8 -  | gen_names i s used = if s mem used
     4.9 -      then gen_names i (Symbol.bump_string s) used
    4.10 -      else s :: gen_names (i-1) (Symbol.bump_string s) used;
    4.11 -
    4.12  fun typs_terms_of used mk_var prfx (Ts, ts) =
    4.13    let
    4.14      fun elim (r as ref (Param S), x) = r := mk_var (x, S)
    4.15 @@ -239,7 +234,7 @@
    4.16  
    4.17      val used' = foldl add_names (foldl add_namesT (used, Ts), ts);
    4.18      val parms = rev (foldl add_parms (foldl add_parmsT ([], Ts), ts));
    4.19 -    val names = gen_names (length parms) (prfx ^ "'a") used';
    4.20 +    val names = Term.invent_names used' (prfx ^ "'a") (length parms);
    4.21    in
    4.22      seq2 elim (parms, names);
    4.23      (map simple_typ_of Ts, map simple_term_of ts)