--- 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 *)