diff -r 8d51b375e926 -r af3df09590f9 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 18 20:50:11 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 18 20:53:39 2012 +0100
@@ -1115,7 +1115,7 @@
 %
 \begin{isamarkuptext}%
 We define a type of finite sequences, with slightly different
-  names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \hyperlink{theory.Main}{\mbox{\isa{Main}}}:%
+  names than the existing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequote}}} that is already in \isa{Main}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{datatype}\isamarkupfalse%