--- a/src/Pure/Thy/thy_parse.ML Mon Nov 03 17:56:39 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML Mon Nov 03 21:04:51 1997 +0100
@@ -551,7 +551,7 @@
val pure_keywords =
- ["end", "ML", "mixfix", "infixr", "infixl", "binder", "global",
+ ["end", "ML", "MLtext", "mixfix", "infixr", "infixl", "binder", "global",
"local", "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]",
"::", "==", "=>", "<="];
@@ -571,7 +571,8 @@
section "instance" "" instance_decl,
section "path" "|> Theory.add_path" name,
section "global" global_path empty_decl,
- section "local" local_path empty_decl];
+ section "local" local_path empty_decl,
+ section "MLtext" "" verbatim];
end;