src/Doc/Isar_Ref/Proof.thy

   that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the
   reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
   \<phi>[t]\<close>.
 
   @{rail \<open>
-    @@{command fix} @{syntax "fixes"}
+    @@{command fix} @{syntax vars}
     ;
     (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}
     ;
     concl: (@{syntax props} + @'and')
     ;
     prems: (@'if' (@{syntax props'} + @'and'))?
     ;
-    @@{command define} (@{syntax "fixes"} + @'and')
-      @'where' (@{syntax props} + @'and') @{syntax for_fixes}
+    @@{command define} @{syntax vars} @'where'
+      (@{syntax props} + @'and') @{syntax for_fixes}
     ;
     @@{command def} (def + @'and')
     ;
     def: @{syntax thmdecl}? \<newline>
       @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?

     ;
     conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
     ;
     @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
     ;
-    @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'
+    @{syntax_def obtain_case}: @{syntax vars} @'where'
       (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
 
   \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,
   eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target

   delegated to an Isar proof, which often involves automated tools.
 
   @{rail \<open>
     @@{command consider} @{syntax obtain_clauses}
     ;
-    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
+    @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>
       @'where' concl prems @{syntax for_fixes}
     ;
     concl: (@{syntax props} + @'and')
     ;
     prems: (@'if' (@{syntax props'} + @'and'))?
     ;
-    @@{command guess} (@{syntax "fixes"} + @'and')
+    @@{command guess} @{syntax vars}
   \<close>}
 
   \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)
   \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting
   into separate subgoals, such that each case involves new parameters and