# HG changeset patch
# User wenzelm
# Date 1165683942 -3600
# Node ID 88661e47147d4e80dcc5919d7d21f44e084021e9
# Parent  25239591e732212093e9f6e1705f6261eb8ab519
renamed reserved to reserved_names;
added reserved: Name.context;

diff -r 25239591e732 -r 88661e47147d src/Pure/General/ml_syntax.ML
--- a/src/Pure/General/ml_syntax.ML	Sat Dec 09 18:05:41 2006 +0100
+++ b/src/Pure/General/ml_syntax.ML	Sat Dec 09 18:05:42 2006 +0100
@@ -7,7 +7,8 @@
 
 signature ML_SYNTAX =
 sig
-  val reserved: string list
+  val reserved_names: string list
+  val reserved: Name.context
   val is_reserved: string -> bool
   val is_identifier: string -> bool
   val str_of_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
@@ -21,7 +22,7 @@
 
 (* reserved words *)
 
-val reserved =
+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",
@@ -29,7 +30,8 @@
   "eqtype", "functor", "include", "sharing", "sig", "signature",
   "struct", "structure", "where"];
 
-val is_reserved = member (op =) reserved;
+val reserved = Name.make_context reserved_names;
+val is_reserved = Name.is_declared reserved;
 
 
 (* identifiers *)