--- a/src/Pure/Isar/keyword.ML Wed Oct 20 09:31:37 2021 +0200
+++ b/src/Pure/Isar/keyword.ML Wed Oct 20 10:47:34 2021 +0200
@@ -51,6 +51,7 @@
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 is_keyword: keywords -> string -> bool
val is_command: keywords -> string -> bool
val is_literal: keywords -> string -> bool
@@ -199,6 +200,9 @@
val commands' = Symtab.update (name, entry) commands;
in (minor, major', commands') end));
+val add_minor_keywords =
+ add_keywords o map (fn name => ((name, Position.none), no_spec));
+
(* keyword status *)
--- a/src/Pure/Tools/find_consts.ML Wed Oct 20 09:31:37 2021 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed Oct 20 10:47:34 2021 +0200
@@ -140,8 +140,7 @@
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
Parse.typ >> Loose;
-val query_keywords =
- Keyword.add_keywords [((":", \<^here>), Keyword.no_spec)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_minor_keywords [":"] Keyword.empty_keywords;
in
--- a/src/Pure/Tools/find_theorems.ML Wed Oct 20 09:31:37 2021 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Oct 20 10:47:34 2021 +0200
@@ -524,8 +524,7 @@
Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
Parse.term >> Pattern;
-val query_keywords =
- Keyword.add_keywords [((":", \<^here>), Keyword.no_spec)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_minor_keywords [":"] Keyword.empty_keywords;
in