diff -r 5d63184c10c7 -r 150a8a1eae1a doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:40 2008 +0200
@@ -1050,9 +1050,7 @@
     ;
 
     'code\_class' (class + 'and') \\
-      ( ( '(' target \\
-        ( ( string ('where' \\
-          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
+      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
     ;
 
     'code\_instance' (( typeconstructor '::' class ) + 'and') \\
@@ -1135,10 +1133,9 @@
   serialization deletes an existing serialization.
 
   \item [@{command (HOL) "code_class"}] associates a list of classes
-  with target-specific class names; in addition, constants associated
-  with this class may be given target-specific names used for instance
-  declarations; omitting a serialization deletes an existing
-  serialization.  This applies only to \emph{Haskell}.
+  with target-specific class names; omitting a
+  serialization deletes an existing serialization.
+  This applies only to \emph{Haskell}.
 
   \item [@{command (HOL) "code_instance"}] declares a list of type
   constructor / class instance relations as ``already present'' for a