--- 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%