# HG changeset patch
# User wenzelm
# Date 878587491 -3600
# Node ID 884968ad30da5a6bab4e3df9b79a127319f9dc7b
# Parent  f746af27164b518c1867dc9d19e006984288d688
added MLtext section;

diff -r f746af27164b -r 884968ad30da src/Pure/Thy/thy_parse.ML
--- 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;