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;