diff -r 50f42116ebdb -r cb6634eb8926 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Oct 13 13:05:23 2010 +0100
@@ -1081,8 +1081,8 @@
 
 ML {* Binding.pos_of @{binding here} *}
 
-text {* \medskip That position can be also printed in a message as
-  follows. *}
+text {* \medskip\noindent That position can be also printed in a
+  message as follows. *}
 
 ML_command {*
   writeln