diff -r 245ff8661b8c -r c708ea5b109a doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Aug 20 18:07:49 2007 +0200
@@ -32,7 +32,7 @@
 \newcommand{\isasymSHOW}{\cmd{show}}
 \newcommand{\isasymNOTE}{\cmd{note}}
 \newcommand{\isasymIN}{\cmd{in}}
-\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
+\newcommand{\isasymEXPORTCODE}{\cmd{export\_code}}
 \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
 \newcommand{\isasymCODECONST}{\cmd{code\_const}}
 \newcommand{\isasymCODETYPE}{\cmd{code\_type}}