diff -r 0928909af6aa -r 4301e9ea1c54 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Dec 23 08:31:14 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Dec 23 08:31:14 2009 +0100
@@ -1150,7 +1150,7 @@
   \end{matharray}
 
   \begin{rail}
-    'export\_code' ( constexpr + ) ? \\
+    'export\_code' ( constexpr + ) \\
       ( ( 'in' target ( 'module\_name' string ) ? \\
         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     ;
@@ -1227,10 +1227,8 @@
 
   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} is the canonical interface for
   generating and serializing code: for a given list of constants, code
-  is generated for the specified target languages.  Abstract code is
-  cached incrementally.  If no constant is given, the currently cached
-  code is serialized.  If no serialization instruction is given, only
-  abstract code is cached.
+  is generated for the specified target languages.  If no serialization
+  instruction is given, only abstract code is generated internally.
 
   Constants may be specified by giving them literally, referring to
   all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
@@ -1249,18 +1247,19 @@
   code internally in the context of the current ML session.
 
   Serializers take an optional list of arguments in parentheses.  For
-  \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
+  \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
+  explicit module signatures.
+  
+  For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
   declaration.
 
   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
   representing the corresponding program containing all given
-  constants; if no constants are given, the currently cached code
-  theorems are printed.
+  constants.
 
   \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
   theorems representing the corresponding program containing all given
-  constants; if no constants are given, the currently cached code
-  theorems are visualized.
+  constants.
 
   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
   for a logical type.