diff -r 056255ade52a -r 4e74209f113e doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 10 06:45:53 2008 +0200
@@ -997,7 +997,7 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ('func' | 'inline') ( 'del' )?
+    'code' ( 'inline' ) ? ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1081,13 +1081,13 @@
   are not required to have a definition by means of defining equations;
   if needed these are implemented by program abort instead.
 
-  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
-  with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
+  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
+  with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
   code generation.  Usually packages introducing defining equations
   provide a reasonable default setup for selection.
 
   \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
-  option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
+  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
   applied as rewrite rules to any defining equation during
   preprocessing.