# HG changeset patch
# User wenzelm
# Date 1189877177 -7200
# Node ID 57599da58045b686d038a8c0dabcc69f1c3114ad
# Parent  6491d89ba76cd5e37aa5f79ec9edf50c5a95fc80
ML_Lex.keywords;
tuned comments;

diff -r 6491d89ba76c -r 57599da58045 src/Pure/ML/ml_syntax.ML
--- 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;