src/Pure/General/symbol.ML
changeset 17412 e26cb20ef0cc
parent 17221 6cd180204582
child 17756 d4a35f82fbb4
--- a/src/Pure/General/symbol.ML	Thu Sep 15 17:16:55 2005 +0200
+++ b/src/Pure/General/symbol.ML	Thu Sep 15 17:16:56 2005 +0200
@@ -350,7 +350,7 @@
     else if is_ascii_quasi s then Quasi
     else if is_ascii_blank s then Blank
     else if is_char s then Other
-    else if_none (Symtab.curried_lookup symbol_kinds s) Other;
+    else if_none (Symtab.lookup symbol_kinds s) Other;
 end;
 
 fun is_letter s = kind s = Letter;