diff -r 3f19e324ff59 -r 528a2ba8fa74 doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu May 05 23:23:02 2011 +0200
@@ -304,7 +304,7 @@
     @{syntax_def typespec}:
       (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
     ;
-    @{syntax_def typespecsorts}:
+    @{syntax_def typespec_sorts}:
       (() | (@{syntax typefree} ('::' @{syntax sort})?) |
         '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
   "}
@@ -319,9 +319,9 @@
   This works both for @{syntax term} and @{syntax prop}.
 
   @{rail "
-    @{syntax_def termpat}: '(' (@'is' @{syntax term} +) ')'
+    @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
     ;
-    @{syntax_def proppat}: '(' (@'is' @{syntax prop} +) ')'
+    @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
   "}
 
   \medskip Declarations of local variables @{text "x :: \<tau>"} and
@@ -335,7 +335,7 @@
   @{rail "
     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
     ;
-    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax proppat}? +)
+    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
   "}
 
   The treatment of multiple declarations corresponds to the