tuned signature;

--- a/src/Pure/Isar/outer_syntax.ML	Mon Dec 04 23:10:52 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Dec 05 14:03:10 2017 +0100
@@ -183,10 +183,10 @@
   Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
 
 fun parse_command thy =
-  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
+  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     let
       val keywords = Thy_Header.get_keywords thy;
-      val command_tags = Parse.command_ -- Parse.tags;
+      val command_tags = Parse.command -- Parse.tags;
       val tr0 =
         Toplevel.empty
         |> Toplevel.name name

--- a/src/Pure/Isar/parse.ML	Mon Dec 04 23:10:52 2017 +0100
+++ b/src/Pure/Isar/parse.ML	Tue Dec 05 14:03:10 2017 +0100
@@ -15,7 +15,7 @@
   val position: 'a parser -> ('a * Position.T) parser
   val input: 'a parser -> Input.source parser
   val inner_syntax: 'a parser -> string parser
-  val command_: string parser
+  val command: string parser
   val keyword: string parser
   val short_ident: string parser
   val long_ident: string parser
@@ -32,7 +32,7 @@
   val verbatim: string parser
   val cartouche: string parser
   val eof: string parser
-  val command: string -> string parser
+  val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
   val keyword_markup: bool * Markup.T -> string -> string parser
   val keyword_improper: string -> string parser
@@ -173,7 +173,7 @@
   group (fn () => Token.str_of_kind k)
     (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
 
-val command_ = kind Token.Command;
+val command = kind Token.Command;
 val keyword = kind Token.Keyword;
 val short_ident = kind Token.Ident;
 val long_ident = kind Token.Long_Ident;
@@ -189,7 +189,7 @@
 val cartouche = kind Token.Cartouche;
 val eof = kind Token.EOF;
 
-fun command x =
+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;

--- a/src/Pure/Thy/thy_header.ML	Mon Dec 04 23:10:52 2017 +0100
+++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 14:03:10 2017 +0100
@@ -160,19 +160,19 @@
 (* read header *)
 
 val heading =
-  (Parse.command chapterN ||
-    Parse.command sectionN ||
-    Parse.command subsectionN ||
-    Parse.command subsubsectionN ||
-    Parse.command paragraphN ||
-    Parse.command subparagraphN ||
-    Parse.command textN ||
-    Parse.command txtN ||
-    Parse.command text_rawN) --
+  (Parse.command_name chapterN ||
+    Parse.command_name sectionN ||
+    Parse.command_name subsectionN ||
+    Parse.command_name subsubsectionN ||
+    Parse.command_name paragraphN ||
+    Parse.command_name subparagraphN ||
+    Parse.command_name textN ||
+    Parse.command_name txtN ||
+    Parse.command_name text_rawN) --
   Parse.tags -- Parse.!!! Parse.document_source;
 
 val header =
-  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
+  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
 
 fun token_source pos =
   Symbol.explode