--- 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;
--- 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;