Changed some mem calls to mem_string for greater efficiency (not that it could matter)
authorpaulson
Wed Oct 30 11:19:09 1996 +0100 (1996-10-30)
changeset 2138056dead45ae8
parent 2137 afc15c2fd5b5
child 2139 2c59b204b540
Changed some mem calls to mem_string for greater efficiency (not that it could matter)
src/Pure/sign.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/sign.ML	Wed Oct 30 11:17:54 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Oct 30 11:19:09 1996 +0100
     1.3 @@ -184,13 +184,13 @@
     1.4  (** pretty printing of terms and types **)
     1.5  
     1.6  fun pretty_term (Sg {syn, stamps, ...}) =
     1.7 -  let val curried = "CPure" mem (map ! stamps);
     1.8 +  let val curried = "CPure" mem_string (map ! stamps);
     1.9    in Syntax.pretty_term curried syn end;
    1.10  
    1.11  fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
    1.12  
    1.13  fun string_of_term (Sg {syn, stamps, ...}) =
    1.14 -  let val curried = "CPure" mem (map ! stamps);
    1.15 +  let val curried = "CPure" mem_string (map ! stamps);
    1.16    in Syntax.string_of_term curried syn end;
    1.17  
    1.18  fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
     2.1 --- a/src/Pure/term.ML	Wed Oct 30 11:17:54 1996 +0100
     2.2 +++ b/src/Pure/term.ML	Wed Oct 30 11:19:09 1996 +0100
     2.3 @@ -472,8 +472,8 @@
     2.4  (*Makes a variant of the name c distinct from the names in bs.
     2.5    First attaches the suffix "a" and then increments this. *)
     2.6  fun variant bs c : string =
     2.7 -  let fun vary2 c = if (c mem bs) then  vary2 (bump_string c)  else  c
     2.8 -      fun vary1 c = if (c mem bs) then  vary2 (c ^ "a")  else  c
     2.9 +  let fun vary2 c = if (c mem_string bs) then  vary2 (bump_string c)  else  c
    2.10 +      fun vary1 c = if (c mem_string bs) then  vary2 (c ^ "a")  else  c
    2.11    in  vary1 (if c="" then "u" else c)  end;
    2.12  
    2.13  (*Create variants of the list of names, with priority to the first ones*)