clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);

--- a/src/Doc/Isar_Ref/Proof.thy	Fri Apr 17 19:49:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Apr 18 20:44:55 2015 +0200
@@ -444,9 +444,9 @@
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
-    conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
+    conclusion: @'shows' goal | @'obtains' (@{syntax parname}? obtain_case + '|')
     ;
-    case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
+    obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
 
   \begin{description}