
diff -r b416573f1807 -r 3dd426ae6bea doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Wed Oct 19 23:07:48 2011 +0200
@@ -236,15 +236,6 @@
     \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 @{text "generic code
-    generator"}, to the other as @{text "SML code generator"}.
-  \end{warn}
 *}
 
 end




