doc-src/IsarRef/Thy/HOL_Specific.thy

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 15 21:29:23 2012 +0100
@@ -864,7 +864,9 @@
 
   @{rail "
     @@{command (HOL) record} @{syntax typespec_sorts} '=' \\
-      (@{syntax type} '+')? (@{syntax constdecl} +)
+      (@{syntax type} '+')? (constdecl +)
+    ;
+    constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
   "}
 
   \begin{description}