# HG changeset patch
# User wenzelm
# Date 940941290 -7200
# Node ID 220892918bd1d9f8648342e039b1a033a8b00461
# Parent  2010ae0393ca02f0c7276186d02b299eea5dba1a
added opt_unit (from isar_syn.ML);

diff -r 2010ae0393ca -r 220892918bd1 src/Pure/Isar/outer_parse.ML
--- 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 *)