--- a/src/HOL/Library/document/root.tex Thu Dec 14 19:37:27 2000 +0100
+++ b/src/HOL/Library/document/root.tex Thu Dec 14 19:37:43 2000 +0100
@@ -26,9 +26,10 @@
\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
\renewcommand{\isamarkupheader}[1]%
-{\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
+{\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
+#1%
\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
-\markright{THEORY~``\isabellecontext''}
+\markright{THEORY~``\isabellecontext''}%
\ifthenelse{\equal{}{\isabelleauthor}}{}%
{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}