src/Pure/Isar/outer_parse.ML

   val group: string -> (token list -> 'a) -> token list -> 'a
   val !!! : (token list -> 'a) -> token list -> 'a
   val !!!! : (token list -> 'a) -> token list -> 'a
   val $$$ : string -> token list -> string * token list
   val semicolon: token list -> string * token list
+  val underscore: token list -> string * token list
   val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
   val command: token list -> string * token list
   val keyword: token list -> string * token list
   val short_ident: token list -> string * token list
   val long_ident: token list -> string * token list

   group (T.str_of_kind T.Keyword ^ " " ^ quote x)
     (Scan.one (T.keyword_with (equal x)) >> T.val_of);
 
 val semicolon = $$$ ";";
 
+val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val nat = number >> (fst o Term.read_int o Symbol.explode);
 
 val not_eof = Scan.one T.not_eof;
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();