1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 14 14:20:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 14 14:53:44 2010 +0200
     1.3 @@ -998,9 +998,9 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    'export\_code' ( constexpr + ) \\
     1.8 -      ( ( 'in' target ( 'module\_name' string ) ? \\
     1.9 -        'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
    1.10 +     'export\_code' ( constexpr + ) \\
    1.11 +       ( ( 'in' target ( 'module\_name' string ) ? \\
    1.12 +        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
    1.13      ;
    1.14  
    1.15      const: term
    1.16 @@ -1091,7 +1091,7 @@
    1.17    For \emph{SML} and \emph{OCaml}, the file specification refers to a
    1.18    single file; for \emph{Haskell}, it refers to a whole directory,
    1.19    where code is generated in multiple files reflecting the module
    1.20 -  hierarchy.  The file specification ``@{text "-"}'' denotes standard
    1.21 +  hierarchy.  Omitting the file specification denotes standard
    1.22    output.
    1.23  
    1.24    Serializers take an optional list of arguments in parentheses.  For