# HG changeset patch
# User wenzelm
# Date 1160519255 -7200
# Node ID 555d27f2c210ae712d6d999bfd36a436ef656843
# Parent  f342e82f4e58c41227b88f324c170717305d0144
added opt_begin;

diff -r f342e82f4e58 -r 555d27f2c210 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Oct 11 00:27:34 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Oct 11 00:27:35 2006 +0200
@@ -39,6 +39,7 @@
   val tags: token list -> string list * token list
   val opt_unit: token list -> unit * token list
   val opt_keyword: string -> token list -> bool * token list
+  val opt_begin: token list -> bool * 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
@@ -190,6 +191,8 @@
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
 
+val opt_begin = Scan.optional ($$$ "begin" >> K true) false;
+
 
 (* enumerations *)