diff -r 419116f1157a -r e23770bc97c8 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 08:44:44 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Feb 26 08:48:33 2009 -0800
@@ -3,14 +3,14 @@
 \def\isabellecontext{ML}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %