diff -r 6573e6d64ec8 -r 1c54ebc68394 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Fri Nov 14 11:19:14 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Fri Nov 14 17:07:06 2014 +0100
@@ -503,19 +503,12 @@
   single argument).
 
   \medskip Text blocks are introduced by the commands \bfindex{text}
-  and \bfindex{txt}, for theory and proof contexts, respectively.
-  Each takes again a single $text$ argument, which is interpreted as a
-  free-form paragraph in {\LaTeX} (surrounded by some additional
-  vertical space).  This behavior may be changed by redefining the
-  {\LaTeX} environments of \verb,isamarkuptext, or
-  \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
-  text style of the body is determined by \verb,\isastyletext, and
-  \verb,\isastyletxt,; the default setup uses a smaller font within
-  proofs.  This may be changed as follows:
-
-\begin{verbatim}
-  \renewcommand{\isastyletxt}{\isastyletext}
-\end{verbatim}
+  and \bfindex{txt}. Each takes again a single $text$ argument,
+  which is interpreted as a free-form paragraph in {\LaTeX}
+  (surrounded by some additional vertical space).  The typesetting
+  may be changed by redefining the {\LaTeX} environments of
+  \verb,isamarkuptext, or \verb,isamarkuptxt,, respectively
+  (via \verb,\renewenvironment,).
 
   \medskip The $text$ part of Isabelle markup commands essentially
   inserts \emph{quoted material} into a formal text, mainly for