# HG changeset patch
# User wenzelm
# Date 976819063 -3600
# Node ID 2cc6415c18018fe97f6cb2cb4a218a06d9056dd1
# Parent  337c00fd385b465d9cc75b163c5e9fd787a4b0e6
tuned;

diff -r 337c00fd385b -r 2cc6415c1801 src/HOL/Library/document/root.tex
--- 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}}}