diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -628,9 +628,9 @@
 %
 \begin{isamarkuptext}%
 Typical data structures implemented by representations involving
-  invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}}
+  invariants are available in the library, theory \isa{Mapping}
   specifies key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping});
-  these can be implemented by red-black-trees (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
+  these can be implemented by red-black-trees (theory \isa{RBT}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %