diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Wed Oct 19 23:07:48 2011 +0200
@@ -560,15 +560,7 @@
 
     \begin{center}\textit{Happy proving, happy hacking!}\end{center}
 
-  \end{minipage}}}\end{center}
-
-  \begin{warn}
-    There is also a more ancient code generator in Isabelle by Stefan
-    Berghofer \cite{Berghofer-Nipkow:2002}.  Although its
-    functionality is covered by the code generator presented here, it
-    will sometimes show up as an artifact.  In case of ambiguity, we
-    will refer to the framework described here as \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
-  \end{warn}%
+  \end{minipage}}}\end{center}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %