# HG changeset patch
# User wenzelm
# Date 1429384385 -7200
# Node ID 9cfc45235c2739d6b8e4504ce96ed38eaa4a6728
# Parent  add41579a1d3e70bc6f4eb82dc40c334a4992817# Parent  2506f17d273941fe73278d7dc61c2b141f547d63
merged

diff -r add41579a1d3 -r 9cfc45235c27 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Apr 18 19:36:07 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Apr 18 21:13:05 2015 +0200
@@ -205,7 +205,7 @@
     @{syntax_def name}: @{syntax ident} | @{syntax symident} |
       @{syntax string} | @{syntax nat}
     ;
-    @{syntax_def parname}: '(' @{syntax name} ')'
+    @{syntax_def par_name}: '(' @{syntax name} ')'
     ;
     @{syntax_def nameref}: @{syntax name} | @{syntax longident}
   \<close>}
diff -r add41579a1d3 -r 9cfc45235c27 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sat Apr 18 19:36:07 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Apr 18 21:13:05 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 par_name}? obtain_case + '|')
     ;
-    case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
+    obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
 
   \begin{description}
@@ -989,7 +989,7 @@
   occur in the conclusion.
 
   @{rail \<open>
-    @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')
+    @@{command obtain} @{syntax par_name}? (@{syntax vars} + @'and')
       @'where' (@{syntax props} + @'and')
     ;
     @@{command guess} (@{syntax vars} + @'and')