src/Pure/term.ML
changeset 19014 f70ced571ba8
parent 18995 ff4e4773cc7c
child 19065 82e2d66f995b
     1.1 --- a/src/Pure/term.ML	Sat Feb 11 17:17:48 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Sat Feb 11 17:17:49 2006 +0100
     1.3 @@ -190,6 +190,7 @@
     1.4    val maxidx_typ: typ -> int -> int
     1.5    val maxidx_typs: typ list -> int -> int
     1.6    val maxidx_term: term -> int -> int
     1.7 +  val variant_name: (string -> bool) -> string -> string
     1.8    val invent_names: string list -> string -> int -> string list
     1.9    val dest_abs: string * typ * term -> string * term
    1.10    val bound: int -> string
    1.11 @@ -1058,16 +1059,18 @@
    1.12  
    1.13  (*** Printing ***)
    1.14  
    1.15 -(*Makes a variant of a name distinct from the names in 'used'.
    1.16 -  First attaches the suffix and then increments this;
    1.17 -  preserves a suffix of underscores "_". *)
    1.18 -fun variant used name =
    1.19 +(*Makes a variant of a name distinct from already used names.  First
    1.20 +  attaches the suffix and then increments this; preserves a suffix of
    1.21 +  underscores "_". *)
    1.22 +fun variant_name used name =
    1.23    let
    1.24 -    val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
    1.25 -    fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c;
    1.26 -    fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c;
    1.27 +    val (c, u) = pairself implode (Library.take_suffix (fn s => s = "_") (Symbol.explode name));
    1.28 +    fun vary2 c = if used (c ^ u) then vary2 (Symbol.bump_string c) else c;
    1.29 +    fun vary1 c = if used (c ^ u) then vary2 (Symbol.bump_init c) else c;
    1.30    in vary1 (if c = "" then "u" else c) ^ u end;
    1.31  
    1.32 +fun variant used_names = variant_name (member (op =) used_names);
    1.33 +
    1.34  (*Create variants of the list of names, with priority to the first ones*)
    1.35  fun variantlist ([], used) = []
    1.36    | variantlist(b::bs, used) =