tuned;
authorwenzelm
Fri, 16 Apr 2004 21:03:40 +0200
changeset 14609 663e0e435866
parent 14608 9f9d651d676b
child 14610 9c2e31e483b2
tuned;
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;