src/Pure/Isar/keyword.ML

   val document_heading_spec: spec
   val document_body_spec: spec
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
   val major_keywords: keywords -> Scan.lexicon
-  val no_command_keywords: keywords -> keywords
   val empty_keywords: keywords
   val merge_keywords: keywords * keywords -> keywords
   val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords
   val add_minor_keywords: string list -> keywords -> keywords
   val add_major_keywords: string list -> keywords -> keywords
+  val no_major_keywords: 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

   Keywords {minor = minor, major = major, commands = commands};
 
 fun map_keywords f (Keywords {minor, major, commands}) =
   make_keywords (f (minor, major, commands));
 
-val no_command_keywords =
-  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
-
 
 (* build keywords *)
 
 val empty_keywords =
   make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);

   add_keywords o map (fn name => ((name, Position.none), no_spec));
 
 val add_major_keywords =
   add_keywords o map (fn name => ((name, Position.none), (diag, [])));
 
+val no_major_keywords =
+  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
+
 
 (* keyword status *)
 
 fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s);
 fun is_command (Keywords {commands, ...}) = Symtab.defined commands;