diff -r 19cd739f4b0a -r e00a2edd1dc6 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 28 15:10:34 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 28 17:25:46 2010 +0200
@@ -750,7 +750,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 @{text "swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times> \<alpha>"}, or the
   combinator @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"} that is not even
   defined in our library.
@@ -787,7 +787,7 @@
   to the right: @{text "insert a"} is a function @{text "\<beta> \<rightarrow> \<beta>"} to
   insert a value @{text "a"}.  These can be composed naturally as
   @{text "insert c \<circ> insert b \<circ> 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.
 *}
@@ -1138,9 +1138,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,