diff -r 19cd739f4b0a -r e00a2edd1dc6 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Oct 28 15:10:34 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Oct 28 17:25:46 2010 +0200
@@ -948,7 +948,7 @@
 
   This can be avoided by \emph{canonical argument order}, which
   observes certain standard patterns and minimizes adhoc permutations
-  in their application.  In Isabelle/ML, large portions text can be
+  in their application.  In Isabelle/ML, large portions of text can be
   written without ever using \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}}, or the
   combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}} that is not even
   defined in our library.
@@ -983,7 +983,7 @@
   to the right: \isa{insert\ a} is a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} to
   insert a value \isa{a}.  These can be composed naturally as
   \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}.  The slightly awkward
-  inversion if the composition order is due to conventional
+  inversion of the composition order is due to conventional
   mathematical notation, which can be easily amended as explained
   below.%
 \end{isamarkuptext}%
@@ -1450,9 +1450,9 @@
   language definition.  It was excluded from the SML97 version to
   avoid its malign impact on ML program semantics, but without
   providing a viable alternative.  Isabelle/ML recovers physical
-  interruptibility (which an indispensable tool to implement managed
-  evaluation of command transactions), but requires user code to be
-  strictly transparent wrt.\ interrupts.
+  interruptibility (which is an indispensable tool to implement
+  managed evaluation of command transactions), but requires user code
+  to be strictly transparent wrt.\ interrupts.
 
   \begin{warn}
   Isabelle/ML user code needs to terminate promptly on interruption,