src/Pure/Isar/parse.ML

   val maybe: 'a parser -> 'a option parser
   val tag_name: string parser
   val tags: string list parser
   val opt_unit: unit parser
   val opt_keyword: string -> bool parser
+  val opt_bang: bool parser
   val begin: string parser
   val opt_begin: bool parser
   val nat: int parser
   val int: int parser
   val real: real parser

 val tag_name = group (fn () => "tag name") (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
 fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
+val opt_bang = Scan.optional ($$$ "!" >> K true) false;
 
 val begin = $$$ "begin";
 val opt_begin = Scan.optional (begin >> K true) false;
 
 

     position xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
 
 val xthms1 = Scan.repeat1 xthm;
 
 end;
-