--- a/src/HOL/Hoare/document/root.tex Sun Nov 02 17:23:48 2014 +0100
+++ b/src/HOL/Hoare/document/root.tex Sun Nov 02 17:27:22 2014 +0100
@@ -7,8 +7,6 @@
\urlstyle{rm}
\isabellestyle{it}
-\renewcommand{\isamarkupheader}[1]{#1}
-
\begin{document}
\title{Hoare Logic}