diff -r a461dd80f83c -r 7935b334893e doc-src/Codegen/codegen.tex
--- a/doc-src/Codegen/codegen.tex	Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/codegen.tex	Fri Aug 13 14:40:15 2010 +0200
@@ -31,11 +31,11 @@
 \clearfirst
 
 \input{Thy/document/Introduction.tex}
-\input{Thy/document/Program.tex}
+\input{Thy/document/Foundations.tex}
+\input{Thy/document/Refinement.tex}
 \input{Thy/document/Inductive_Predicate.tex}
 \input{Thy/document/Adaptation.tex}
 \input{Thy/document/Further.tex}
-\input{Thy/document/ML.tex}
 
 \begingroup
 \bibliographystyle{plain} \small\raggedright\frenchspacing