diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -30,7 +30,7 @@
   \cite{scala-overview-tech-report}.
 
   To profit from this tutorial, some familiarity and experience with
-  \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.%
+  \isa{HOL} \cite{isa-tutorial} and its basic theories is assumed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %