diff -r 788e902f3c59 -r b8d89db3e238 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -86,13 +86,12 @@
   \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
   \end{center}
 
-  \noindent When a definitional package is finished, the auxiliary
-  context is reset to the target context.  The target now holds
-  definitions for terms and theorems that stem from the hypothetical
-  @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by
-  the particular target policy (see
-  \cite[\S4--5]{Haftmann-Wenzel:2009} for details).
-*}
+  When a definitional package is finished, the auxiliary context is
+  reset to the target context.  The target now holds definitions for
+  terms and theorems that stem from the hypothetical @{text
+  "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
+  particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
+  for details).  *}
 
 text %mlref {*
   \begin{mldecls}