--- 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;