diff -r 92715b528e78 -r 77d239840285 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Mon May 02 16:33:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon May 02 17:06:40 2011 +0200
@@ -444,7 +444,7 @@
   
     goal: (@{syntax props} + @'and')
     ;
-    longgoal: @{syntax thmdecl}? (@{syntax contextelem} * ) conclusion
+    longgoal: @{syntax thmdecl}? (@{syntax context_elem} * ) conclusion
     ;
     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
     ;
@@ -458,7 +458,7 @@
   \<phi>"} to be put back into the target context.  An additional @{syntax
   context} specification may build up an initial proof context for the
   subsequent claim; this includes local definitions and syntax as
-  well, see the definition of @{syntax contextelem} in
+  well, see the definition of @{syntax context_elem} in
   \secref{sec:locale}.
   
   \item @{command "theorem"}~@{text "a: \<phi>"} and @{command
@@ -1278,7 +1278,7 @@
     ;
     @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
     ;
-    @@{method coinduct} insts taking rule?
+    @@{method coinduct} @{syntax insts} taking rule?
     ;
 
     rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +)
@@ -1289,7 +1289,7 @@
     ;
     arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
     ;
-    taking: 'taking' ':' insts
+    taking: 'taking' ':' @{syntax insts}
   "}
 
   \begin{description}