src/Pure/Isar/parse.ML

   val keyword_with: (string -> bool) -> string parser
   val keyword_markup: bool * Markup.T -> string -> string parser
   val keyword_improper: string -> string parser
   val $$$ : string -> string parser
   val reserved: string -> string parser
-  val semicolon: string parser
   val underscore: string parser
   val maybe: 'a parser -> 'a option parser
   val tag_name: string parser
   val tags: string list parser
   val opt_unit: unit parser

 
 fun reserved x =
   group (fn () => "reserved identifier " ^ quote x)
     (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
-val semicolon = $$$ ";";
-
 val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 fun maybe scan = underscore >> K NONE || scan >> SOME;
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);