1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:39 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:40 2008 +0200
     1.3 @@ -1050,9 +1050,7 @@
     1.4      ;
     1.5  
     1.6      'code\_class' (class + 'and') \\
     1.7 -      ( ( '(' target \\
     1.8 -        ( ( string ('where' \\
     1.9 -          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
    1.10 +      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
    1.11      ;
    1.12  
    1.13      'code\_instance' (( typeconstructor '::' class ) + 'and') \\
    1.14 @@ -1135,10 +1133,9 @@
    1.15    serialization deletes an existing serialization.
    1.16  
    1.17    \item [@{command (HOL) "code_class"}] associates a list of classes
    1.18 -  with target-specific class names; in addition, constants associated
    1.19 -  with this class may be given target-specific names used for instance
    1.20 -  declarations; omitting a serialization deletes an existing
    1.21 -  serialization.  This applies only to \emph{Haskell}.
    1.22 +  with target-specific class names; omitting a
    1.23 +  serialization deletes an existing serialization.
    1.24 +  This applies only to \emph{Haskell}.
    1.25  
    1.26    \item [@{command (HOL) "code_instance"}] declares a list of type
    1.27    constructor / class instance relations as ``already present'' for a