diff -r d8d9ea6a6b55 -r 92aad017b847 doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Sat Jul 08 14:01:31 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Sat Jul 08 14:01:40 2006 +0200
@@ -356,7 +356,7 @@
   toplevel state and optional error condition, respectively.  This
   only works after dropping out of the Isar toplevel loop.
 
-  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()| above.
+  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
 
   \end{description}%
 \end{isamarkuptext}%