src/Pure/Tools/find_consts.ML
changeset 58928 23d0ffd48006
parent 58920 2f8168dc0eac
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/Tools/find_consts.ML	Fri Nov 07 16:22:25 2014 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Fri Nov 07 16:36:55 2014 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4  
     1.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
     1.6  
     1.7 -val query_keywords = Keyword.add_keywords (":", NONE) Keyword.empty_keywords;
     1.8 +val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
     1.9  
    1.10  in
    1.11