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