diff -r 26977429b784 -r 0ad69b30b39c doc-src/Codegen/Thy/document/Foundations.tex
--- a/doc-src/Codegen/Thy/document/Foundations.tex	Tue Feb 21 12:45:00 2012 +0100
+++ b/doc-src/Codegen/Thy/document/Foundations.tex	Tue Feb 21 13:10:13 2012 +0100
@@ -31,9 +31,9 @@
   components which can be customised individually.
 
   Conceptually all components operate on Isabelle's logic framework
-  \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.  Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}
+  \isa{Pure}.  Practically, the object logic \isa{HOL}
   provides the necessary facilities to make use of the code generator,
-  mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}.
+  mainly since it is an extension of \isa{Pure}.
 
   The constellation of the different components is visualized in the
   following picture.