tuned keywords;
authorwenzelm
Wed May 20 18:56:59 1998 +0200 (1998-05-20)
changeset 4952addfa29d0481
parent 4951 8637b29e6c38
child 4953 78ff4a45a822
tuned keywords;
src/Pure/Thy/thy_parse.ML
     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,