# HG changeset patch
# User wenzelm
# Date 1082142220 -7200
# Node ID 663e0e435866c0df5ff4f27d8407d070c3097bb6
# Parent  9f9d651d676b0c6d8f1ff87d52072060fa90a2ea
tuned;

diff -r 9f9d651d676b -r 663e0e435866 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Apr 16 21:00:53 2004 +0200
+++ b/src/Pure/General/symbol.ML	Fri Apr 16 21:03:40 2004 +0200
@@ -133,7 +133,7 @@
 in
 val ext_letters = map wrap pre_letters 
 
-fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
+fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem_string ext_letters
 end
      
 fun is_letter s =
@@ -326,4 +326,4 @@
 (* Overwrites versions in Library *)
 
 val quote = Symbol.quote;
-val commas_quote = Symbol.commas_quote;
\ No newline at end of file
+val commas_quote = Symbol.commas_quote;