diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Isar/parse.ML	Sun Aug 26 21:46:50 2012 +0200
@@ -34,6 +34,7 @@
   val verbatim: string parser
   val sync: string parser
   val eof: string parser
+  val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
   val keyword_ident_or_symbolic: string parser
   val $$$ : string -> string parser
@@ -190,6 +191,11 @@
 fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
 val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
 
+fun command_name x =
+  group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
+    (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
+  >> Token.content_of;
+
 fun $$$ x =
   group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
     (keyword_with (fn y => x = y));