diff -r c5e1cce7ace3 -r 963fd2084e8f src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 02 15:27:37 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 02 16:05:43 2014 +0100
@@ -437,7 +437,7 @@
   section headings as well.
 
   \begin{ttbox}
-  header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
+  section {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
   theory Foo_Bar
   imports Main
@@ -459,33 +459,7 @@
   theorem main: \dots
 
   end
-  \end{ttbox}\vspace{-\medskipamount}
-
-  You may occasionally want to change the meaning of markup commands,
-  say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
-  \verb,\isamarkupheader, is a good candidate for some tuning.  We
-  could move it up in the hierarchy to become \verb,\chapter,.
-
-\begin{verbatim}
-  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
-\end{verbatim}
-
-  \noindent Now we must change the document class given in
-  \texttt{root.tex} to something that supports chapters.  A suitable
-  command is \verb,\documentclass{report},.
-
-  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
-  hold the name of the current theory context.  This is particularly
-  useful for document headings:
-
-\begin{verbatim}
-  \renewcommand{\isamarkupheader}[1]
-  {\chapter{#1}\markright{THEORY~\isabellecontext}}
-\end{verbatim}
-
-  \noindent Make sure to include something like
-  \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
-  should have more than two pages to show the effect.
+  \end{ttbox}
 *}