--- a/src/Pure/Isar/outer_parse.ML Tue Oct 26 00:04:05 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML Tue Oct 26 14:34:50 1999 +0200
@@ -26,6 +26,7 @@
val sync: token list -> string * token list
val eof: token list -> string * token list
val not_eof: token list -> token * token list
+ val opt_unit: token list -> unit * token list
val nat: token list -> int * token list
val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
@@ -136,6 +137,8 @@
val not_eof = Scan.one OuterLex.not_eof;
+val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
+
(* enumerations *)