diff -r 245ff8661b8c -r c708ea5b109a doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarRef/logics.tex	Mon Aug 20 18:07:49 2007 +0200
@@ -776,7 +776,7 @@
 \indexisaratt{code inline}
 
 \begin{matharray}{rcl}
-  \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
+  \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
@@ -795,7 +795,7 @@
 \end{matharray}
 
 \begin{rail}
-'code\_gen' ( constexpr + ) ? \\
+'export\_code' ( constexpr + ) ? \\
   ( ( 'in' target ( 'module_name' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
 
 'code\_thms' ( constexpr + ) ?;
@@ -849,7 +849,7 @@
 
 \begin{descr}
 
-\item [$\isarcmd{code_gen}$] is the canonical interface for generating and
+\item [$\isarcmd{export_code}$] is the canonical interface for generating and
   serializing code: for a given list of constants, code is generated for the specified
   target language(s).  Abstract code is cached incrementally.  If no constant is given,
   the currently cached code is serialized.  If no serialization instruction