diff -r 51e026049e4d -r b6fe3b189725 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 26 11:31:22 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 26 15:57:16 2010 +0200
@@ -463,7 +463,7 @@
   \end{enumerate}
 
   Such weakly structured layout should be use with great care.  Here
-  is a counter-example involving @{ML_text let} expressions:
+  are some counter-examples involving @{ML_text let} expressions:
 
   \begin{verbatim}
   (* WRONG *)
@@ -472,6 +472,10 @@
       val y = ...
     in ... end
 
+  fun foo x = let
+    val y = ...
+  in ... end
+
   fun foo x =
   let
     val y = ...