doc-src/IsarRef/Thy/Spec.thy

     ;
     @{syntax_def context_elem}:
       @'fixes' (@{syntax \"fixes\"} + @'and') |
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
-      @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax proppat}? + @'and') |
+      @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
       @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   "}
 
   \begin{description}