--- a/doc-src/IsarRef/Thy/Spec.thy Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu May 05 23:23:02 2011 +0200
@@ -371,7 +371,7 @@
@'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')
"}