--- 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}}