src/Pure/Isar/keyword.ML

--- a/src/Pure/Isar/keyword.ML	Thu Mar 15 14:39:42 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 17:40:26 2012 +0100
@@ -48,6 +48,7 @@
   val status: unit -> unit
   val keyword: string -> unit
   val command: string -> T -> unit
+  val declare: string * (string * string list) option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
   val is_regular: string -> bool
@@ -214,6 +215,9 @@
   change_commands (Symtab.update (name, kind));
   command_status (name, kind));
 
+fun declare (name, NONE) = keyword name
+  | declare (name, SOME kind) = command name (make kind);
+
 
 (* command categories *)