src/Pure/ML/ml_syntax.ML
changeset 50238 98d35a7368bd
parent 43845 d89353d17f54
child 56184 a2bd40830593
--- a/src/Pure/ML/ml_syntax.ML	Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Mon Nov 26 21:10:42 2012 +0100
@@ -34,7 +34,7 @@
 
 (* reserved words *)
 
-val reserved_names = filter Lexicon.is_ascii_identifier ML_Lex.keywords;
+val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords;
 val reserved = Name.make_context reserved_names;
 val is_reserved = Name.is_declared reserved;
 
@@ -42,7 +42,7 @@
 (* identifiers *)
 
 fun is_identifier name =
-  not (is_reserved name) andalso Lexicon.is_ascii_identifier name;
+  not (is_reserved name) andalso Symbol.is_ascii_identifier name;
 
 
 (* literal output -- unformatted *)