src/Pure/ML/ml_syntax.ML
changeset 42290 b1f544c84040
parent 42047 a7a4e04b5386
child 43845 d89353d17f54
--- a/src/Pure/ML/ml_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
@@ -34,7 +34,7 @@
 
 (* reserved words *)
 
-val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
+val reserved_names = filter Lexicon.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 Syntax.is_ascii_identifier name;
+  not (is_reserved name) andalso Lexicon.is_ascii_identifier name;
 
 
 (* literal output -- unformatted *)