diff -r 2c201f3b018e -r 311eee3d63b6 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Oct 16 00:32:34 2001 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue Oct 16 00:33:22 2001 +0200
@@ -14,6 +14,7 @@
   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
@@ -143,6 +144,8 @@
 
 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;