| changeset 59934 | b65c4370f831 |
| parent 59083 | 88b0b1f28adc |
| child 59936 | b8ffc3dc9e24 |
--- a/src/Pure/Tools/find_consts.ML Mon Apr 06 14:09:31 2015 +0200 +++ b/src/Pure/Tools/find_consts.ML Mon Apr 06 16:00:19 2015 +0200 @@ -140,7 +140,7 @@ val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); -val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords; +val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords; in