tuned;

--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Apr 18 20:44:55 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Apr 18 20:46:48 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>}

--- a/src/Doc/Isar_Ref/Proof.thy	Sat Apr 18 20:44:55 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Apr 18 20:46:48 2015 +0200
@@ -444,7 +444,7 @@
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
-    conclusion: @'shows' goal | @'obtains' (@{syntax parname}? obtain_case + '|')
+    conclusion: @'shows' goal | @'obtains' (@{syntax par_name}? obtain_case + '|')
     ;
     obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
@@ -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')