# HG changeset patch
# User paulson
# Date 846670749 -3600
# Node ID 056dead45ae84d2eed7fb0f397fc67a92e4d009b
# Parent  afc15c2fd5b5865746c384c97042e563edff11c8
Changed some mem calls to mem_string for greater efficiency (not that it could matter)

diff -r afc15c2fd5b5 -r 056dead45ae8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Oct 30 11:17:54 1996 +0100
+++ b/src/Pure/sign.ML	Wed Oct 30 11:19:09 1996 +0100
@@ -184,13 +184,13 @@
 (** pretty printing of terms and types **)
 
 fun pretty_term (Sg {syn, stamps, ...}) =
-  let val curried = "CPure" mem (map ! stamps);
+  let val curried = "CPure" mem_string (map ! stamps);
   in Syntax.pretty_term curried syn end;
 
 fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
 
 fun string_of_term (Sg {syn, stamps, ...}) =
-  let val curried = "CPure" mem (map ! stamps);
+  let val curried = "CPure" mem_string (map ! stamps);
   in Syntax.string_of_term curried syn end;
 
 fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
diff -r afc15c2fd5b5 -r 056dead45ae8 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Oct 30 11:17:54 1996 +0100
+++ b/src/Pure/term.ML	Wed Oct 30 11:19:09 1996 +0100
@@ -472,8 +472,8 @@
 (*Makes a variant of the name c distinct from the names in bs.
   First attaches the suffix "a" and then increments this. *)
 fun variant bs c : string =
-  let fun vary2 c = if (c mem bs) then  vary2 (bump_string c)  else  c
-      fun vary1 c = if (c mem bs) then  vary2 (c ^ "a")  else  c
+  let fun vary2 c = if (c mem_string bs) then  vary2 (bump_string c)  else  c
+      fun vary1 c = if (c mem_string bs) then  vary2 (c ^ "a")  else  c
   in  vary1 (if c="" then "u" else c)  end;
 
 (*Create variants of the list of names, with priority to the first ones*)