# HG changeset patch
# User wenzelm
# Date 1705075235 -3600
# Node ID 590a01e3efb49a259520224c11b03a603f2eaecf
# Parent  5c1451900bec54066dc5503fde25527e543e89cc
more accurate syntax: 'obtain' vars are optional;

diff -r 5c1451900bec -r 590a01e3efb4 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Jan 11 16:34:40 2024 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Fri Jan 12 17:00:35 2024 +0100
@@ -419,7 +419,7 @@
     ;
     @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
     ;
-    @{syntax_def obtain_case}: @{syntax vars} @'where'
+    @{syntax_def obtain_case}: (@{syntax vars} @'where')?
       (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>
 
@@ -1344,8 +1344,8 @@
   \<^rail>\<open>
     @@{command consider} @{syntax obtain_clauses}
     ;
-    @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>
-      @'where' concl prems @{syntax for_fixes}
+    @@{command obtain} @{syntax par_name}? \<newline>
+      (@{syntax vars} @'where')? concl prems @{syntax for_fixes}
     ;
     concl: (@{syntax props} + @'and')
     ;