# HG changeset patch
# User wenzelm
# Date 1116773478 -7200
# Node ID bbfb2f1378b3506215e21fd10ff75b37634caea2
# Parent  070ed43b86f8bd0a3531675959961acfcd4cc136
added reserved;

diff -r 070ed43b86f8 -r bbfb2f1378b3 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun May 22 16:51:17 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun May 22 16:51:18 2005 +0200
@@ -31,6 +31,7 @@
   val sync: token list -> string * token list
   val eof: token list -> string * token list
   val $$$ : string -> token list -> string * token list
+  val reserved : string -> token list -> string * token list
   val semicolon: token list -> string * token list
   val underscore: token list -> string * token list
   val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
@@ -148,6 +149,10 @@
   group (T.str_of_kind T.Keyword ^ " " ^ quote x)
     (Scan.one (T.keyword_with (equal x)) >> T.val_of);
 
+fun reserved x =
+  group ("Reserved identifier " ^ quote x)
+    (Scan.one (T.ident_with (equal x)) >> T.val_of);
+
 val semicolon = $$$ ";";
 
 val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;