diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Mon Oct 18 15:35:20 2010 +0100
@@ -65,11 +65,11 @@
 
   \begin{description}
 
-  \item @{ML_type Toplevel.state} represents Isar toplevel states,
-  which are normally manipulated through the concept of toplevel
-  transitions only (\secref{sec:toplevel-transition}).  Also note that
-  a raw toplevel state is subject to the same linearity restrictions
-  as a theory context (cf.~\secref{sec:context-theory}).
+  \item Type @{ML_type Toplevel.state} represents Isar toplevel
+  states, which are normally manipulated through the concept of
+  toplevel transitions only (\secref{sec:toplevel-transition}).  Also
+  note that a raw toplevel state is subject to the same linearity
+  restrictions as a theory context (cf.~\secref{sec:context-theory}).
 
   \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
   operations.  Many operations work only partially for certain cases,