src/Pure/Tools/find_consts.ML
changeset 63429 baedd4724f08
parent 62969 9f394a16c557
child 64556 851ae0e7b09c
--- a/src/Pure/Tools/find_consts.ML	Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/Tools/find_consts.ML	Sun Jul 10 11:18:35 2016 +0200
@@ -140,7 +140,8 @@
   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
   Parse.typ >> Loose;
 
-val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
+val query_keywords =
+  Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
 
 in