src/Pure/Thy/thy_parse.ML
changeset 4952 addfa29d0481
parent 4852 58b5006d36cc
child 4965 06914837e073
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed May 20 18:56:36 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed May 20 18:56:59 1998 +0200
     1.3 @@ -546,9 +546,9 @@
     1.4  
     1.5  
     1.6  val pure_keywords =
     1.7 - ["end", "ML", "MLtext", "mixfix", "infixr", "infixl", "binder", "global",
     1.8 -  "local", "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]",
     1.9 -  "::", "==", "=>", "<="];
    1.10 + ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
    1.11 +  "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>",
    1.12 +  "<="];
    1.13  
    1.14  val pure_sections =
    1.15   [section "classes" "|> Theory.add_classes" class_decls,