diff -r bc04a20e5a37 -r 4e6ab5831cc0 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 16:10:32 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 17:01:47 2015 +0100
@@ -303,21 +303,17 @@
       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     ;
-    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop}
-    (@'for' (@{syntax vars} + @'and'))?
+    dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') @{syntax for_fixes}
     ;
-    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
-    (@'for' (@{syntax vars} + @'and'))?
+    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
+    ;
+    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
     ;
     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
     ;
     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
     ;
     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
-    ;
-
-    dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
-    (@'for' (@{syntax vars} + @'and'))?
   \<close>}
 
 \begin{description}