1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 15 17:45:54 2012 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 19:02:34 2012 +0100
     1.3 @@ -12,15 +12,16 @@
     1.4  (*keep keywords consistent with the parsers, otherwise be prepared for
     1.5    unexpected errors*)
     1.6  
     1.7 -val _ = List.app Keyword.keyword
     1.8 - ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
     1.9 -  "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    1.10 -  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    1.11 -  "advanced", "and", "assumes", "attach", "begin", "binder",
    1.12 -  "constrains", "defines", "fixes", "for", "identifier", "if",
    1.13 -  "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
    1.14 -  "notes", "obtains", "open", "output", "overloaded", "pervasive",
    1.15 -  "shows", "structure", "unchecked", "uses", "where", "|"];
    1.16 +val _ = Context.>> (Context.map_theory
    1.17 +  (fold (fn name => Thy_Header.declare_keyword (name, NONE))
    1.18 +   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.19 +    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    1.20 +    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    1.21 +    "advanced", "and", "assumes", "attach", "begin", "binder",
    1.22 +    "constrains", "defines", "fixes", "for", "identifier", "if",
    1.23 +    "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
    1.24 +    "notes", "obtains", "open", "output", "overloaded", "pervasive",
    1.25 +    "shows", "structure", "unchecked", "uses", "where", "|", "by"]));
    1.26  
    1.27  
    1.28