src/Doc/antiquote_setup.ML
changeset 58919 82a71046dce8
parent 58903 38c72f5f6c2e
child 58923 cb9b69cca999
     1.1 --- a/src/Doc/antiquote_setup.ML	Thu Nov 06 11:44:41 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Thu Nov 06 13:36:19 2014 +0100
     1.3 @@ -191,6 +191,9 @@
     1.4  
     1.5  fun no_check _ _ = true;
     1.6  
     1.7 +fun is_keyword _ (name, _) =
     1.8 +  Keyword.is_keyword (Keyword.get_keywords ()) name;
     1.9 +
    1.10  fun check_command ctxt (name, pos) =
    1.11    is_some (Keyword.command_keyword name) andalso
    1.12      let
    1.13 @@ -259,8 +262,8 @@
    1.14    Theory.setup
    1.15     (entity_antiqs no_check "" @{binding syntax} #>
    1.16      entity_antiqs check_command "isacommand" @{binding command} #>
    1.17 -    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
    1.18 -    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
    1.19 +    entity_antiqs is_keyword "isakeyword" @{binding keyword} #>
    1.20 +    entity_antiqs is_keyword "isakeyword" @{binding element} #>
    1.21      entity_antiqs (can o Method.check_name) "" @{binding method} #>
    1.22      entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
    1.23      entity_antiqs no_check "" @{binding fact} #>