src/Pure/Isar/keyword.ML

   val merge_keywords: keywords * keywords -> keywords
   val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
+  val dest_commands: keywords -> string list
   val command_markup: keywords -> string -> Markup.T option
   val command_kind: keywords -> string -> string option
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
   val is_vacuous: keywords -> string -> bool

 
 fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s);
 fun is_command (Keywords {commands, ...}) = Symtab.defined commands;
 fun is_literal keywords = is_keyword keywords orf is_command keywords;
 
+fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands;
+
 
 (* command keywords *)
 
 fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;