src/Pure/Isar/outer_syntax.ML

 
 signature OUTER_SYNTAX =
 sig
   val help: theory -> string list -> unit
   val print_commands: theory -> unit
-  type command_spec = string * Position.T
-  val command: command_spec -> string ->
+  type command_keyword = string * Position.T
+  val command: command_keyword -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val local_theory': command_spec -> string ->
+  val local_theory': command_keyword -> string ->
     (bool -> local_theory -> local_theory) parser -> unit
-  val local_theory: command_spec -> string ->
+  val local_theory: command_keyword -> string ->
     (local_theory -> local_theory) parser -> unit
-  val local_theory_to_proof': command_spec -> string ->
+  val local_theory_to_proof': command_keyword -> string ->
     (bool -> local_theory -> Proof.state) parser -> unit
-  val local_theory_to_proof: command_spec -> string ->
+  val local_theory_to_proof: command_keyword -> string ->
     (local_theory -> Proof.state) parser -> unit
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list

   in NONE end));
 
 
 (* implicit theory setup *)
 
-type command_spec = string * Position.T;
+type command_keyword = string * Position.T;
 
 fun raw_command (name, pos) comment command_parser =
   let val setup = add_command name (new_command comment command_parser pos)
   in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
 
 fun command (name, pos) comment parse =
   raw_command (name, pos) comment (Parser parse);
 
-fun local_theory_command trans command_spec comment parse =
-  raw_command command_spec comment
+fun local_theory_command trans command_keyword comment parse =
+  raw_command command_keyword comment
     (Private_Parser (fn private =>
       Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
 
 val local_theory' = local_theory_command Toplevel.local_theory';
 val local_theory = local_theory_command Toplevel.local_theory;