src/Pure/Thy/thy_parse.ML
changeset 4103 884968ad30da
parent 4101 e8ad51c88be9
child 4362 e10acc395f0d
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Nov 03 17:56:39 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 03 21:04:51 1997 +0100
     1.3 @@ -551,7 +551,7 @@
     1.4  
     1.5  
     1.6  val pure_keywords =
     1.7 - ["end", "ML", "mixfix", "infixr", "infixl", "binder", "global",
     1.8 + ["end", "ML", "MLtext", "mixfix", "infixr", "infixl", "binder", "global",
     1.9    "local", "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]",
    1.10    "::", "==", "=>", "<="];
    1.11  
    1.12 @@ -571,7 +571,8 @@
    1.13    section "instance" "" instance_decl,
    1.14    section "path" "|> Theory.add_path" name,
    1.15    section "global" global_path empty_decl,
    1.16 -  section "local" local_path empty_decl];
    1.17 +  section "local" local_path empty_decl,
    1.18 +  section "MLtext" "" verbatim];
    1.19  
    1.20  
    1.21  end;