src/Pure/Tools/find_consts.ML
changeset 64556 851ae0e7b09c
parent 63429 baedd4724f08
child 68224 1f7308050349
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Dec 12 17:40:06 2016 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Tue Dec 13 11:51:42 2016 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4    Parse.typ >> Loose;
     1.5  
     1.6  val query_keywords =
     1.7 -  Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
     1.8 +  Keyword.add_keywords [((":", \<^here>), Keyword.no_spec)] Keyword.empty_keywords;
     1.9  
    1.10  in
    1.11