# HG changeset patch
# User wenzelm
# Date 1634719654 -7200
# Node ID 3ba399ecdfaf703fb7c5cdd75ba40b712333f805
# Parent  67c4004495f24a760f71c01e2ba815e8fb9905c4
clarified signature;

diff -r 67c4004495f2 -r 3ba399ecdfaf src/Pure/Isar/keyword.ML
--- 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 *)
 
diff -r 67c4004495f2 -r 3ba399ecdfaf src/Pure/Tools/find_consts.ML
--- 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
 
diff -r 67c4004495f2 -r 3ba399ecdfaf src/Pure/Tools/find_theorems.ML
--- 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