1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 08 16:41:57 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Jul 08 16:48:33 2010 +0200
     1.3 @@ -1016,7 +1016,7 @@
     1.4    \begin{rail}
     1.5      'export\_code' ( constexpr + ) \\
     1.6        ( ( 'in' target ( 'module\_name' string ) ? \\
     1.7 -        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     1.8 +        'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
     1.9      ;
    1.10  
    1.11      const: term
    1.12 @@ -1107,8 +1107,7 @@
    1.13    single file; for \emph{Haskell}, it refers to a whole directory,
    1.14    where code is generated in multiple files reflecting the module
    1.15    hierarchy.  The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
    1.16 -  output.  For \emph{SML}, omitting the file specification compiles
    1.17 -  code internally in the context of the current ML session.
    1.18 +  output.
    1.19  
    1.20    Serializers take an optional list of arguments in parentheses.  For
    1.21    \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits