doc-src/IsarRef/Thy/HOL_Specific.thy

     @@{command (HOL) datatype} (spec + @'and')
     ;
     @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
     ;
 
-    spec: @{syntax parname}? @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
+    spec: @{syntax typespec} @{syntax mixfix}? '=' (cons + '|')
     ;
     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
   "}
 
   \begin{description}