--- 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;