src/Pure/Isar/keyword.ML

--- a/src/Pure/Isar/keyword.ML	Sun Oct 24 16:38:13 2021 +0200
+++ b/src/Pure/Isar/keyword.ML	Sun Oct 24 16:43:54 2021 +0200
@@ -47,12 +47,12 @@
   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
@@ -171,9 +171,6 @@
 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 *)
 
@@ -207,6 +204,9 @@
 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 *)