# HG changeset patch
# User wenzelm
# Date 1415218238 -3600
# Node ID 55160ef37e8f723dd1b33a62f6d8eaffe57c3d2a
# Parent  f49c4f883c58ba79d0c96644fd6199f00e77dc71
more frugal keywords;

diff -r f49c4f883c58 -r 55160ef37e8f src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Nov 05 20:49:30 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Wed Nov 05 21:10:38 2014 +0100
@@ -140,10 +140,12 @@
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
+val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
+
 in
 
 fun read_query pos str =
-  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
+  Outer_Syntax.scan query_keywords pos str
   |> filter Token.is_proper
   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   |> #1;
diff -r f49c4f883c58 -r 55160ef37e8f src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Nov 05 20:49:30 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Nov 05 21:10:38 2014 +0100
@@ -526,10 +526,12 @@
 
 val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
 
+val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
+
 in
 
 fun read_query pos str =
-  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
+  Outer_Syntax.scan query_keywords pos str
   |> filter Token.is_proper
   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   |> #1;