diff -r da45a2f45870 -r 916cb4a28ffd doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Oct 25 11:39:52 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Oct 25 16:14:40 2010 +0200
@@ -829,7 +829,7 @@
 %
 \endisadelimmlantiq
 %
-\isamarkupsubsection{Auxiliary definitions%
+\isamarkupsubsection{Auxiliary definitions \label{sec:logic-aux}%
 }
 \isamarkuptrue%
 %