diff -r fade54fde622 -r d4500b9b220e src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Wed Oct 11 22:55:19 2006 +0200 +++ b/src/Pure/Isar/outer_parse.ML Wed Oct 11 22:55:20 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 begin: token list -> string * 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 @@ -191,7 +192,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; +val begin = $$$ "begin"; +val opt_begin = Scan.optional (begin >> K true) false; (* enumerations *)