src/Pure/Isar/keyword.ML

   val command_keyword: string -> T option
   val command_tags: string -> string list
   val dest: unit -> string list * string list
   val keyword_statusN: string
   val status: unit -> unit
-  val declare: string -> T option -> unit
+  val define: string * T option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
   val is_regular: string -> bool
   val is_heading: string -> bool
   val is_theory_begin: string -> bool

     val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
     val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
   in () end;
 
 
-(* declare *)
-
-fun declare name NONE =
+(* define *)
+
+fun define (name, NONE) =
      (change_keywords (fn ((minor, major), commands) =>
         let
           val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
         in ((minor', major), commands) end);
       keyword_status name)
-  | declare name (SOME kind) =
+  | define (name, SOME kind) =
      (change_keywords (fn ((minor, major), commands) =>
         let
           val major' = Scan.extend_lexicon (Symbol.explode name) major;
           val commands' = Symtab.update (name, kind) commands;
         in ((minor, major'), commands') end);