src/Pure/Tools/find_consts.ML
changeset 58903 38c72f5f6c2e
parent 58893 9e0ecb66d6a7
child 58905 55160ef37e8f
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Nov 05 20:05:32 2014 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Nov 05 20:20:57 2014 +0100
     1.3 @@ -143,7 +143,7 @@
     1.4  in
     1.5  
     1.6  fun read_query pos str =
     1.7 -  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
     1.8 +  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
     1.9    |> filter Token.is_proper
    1.10    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
    1.11    |> #1;