src/Pure/ML/ml_syntax.ML
changeset 24582 57599da58045
parent 24574 e840872e9c7c
child 26362 d9ce159a41d1
--- a/src/Pure/ML/ml_syntax.ML	Sat Sep 15 19:26:06 2007 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sat Sep 15 19:26:17 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Pure/General/ml_syntax.ML
+(*  Title:      Pure/ML/ml_syntax.ML
     ID:         $Id$
     Author:     Makarius
 
@@ -31,14 +31,7 @@
 
 (* reserved words *)
 
-val reserved_names =
- ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
-  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
-  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
-  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
-  "eqtype", "functor", "include", "sharing", "sig", "signature",
-  "struct", "structure", "where"];
-
+val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
 val reserved = Name.make_context reserved_names;
 val is_reserved = Name.is_declared reserved;