# HG changeset patch
# User blanchet
# Date 1380035166 -7200
# Node ID 408c9a3617e36a46bcffed27f31e1a309c9ffc3a
# Parent  62c2f66ff9b2076f14d3a039dec2d5236537e83e
improved rail diagram

diff -r 62c2f66ff9b2 -r 408c9a3617e3 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Sep 24 16:59:14 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Sep 24 17:06:06 2013 +0200
@@ -2023,10 +2023,10 @@
 Primitive corecursive definitions have the following general syntax:
 
 @{rail "
-  (@@{command_def primcorec} | @@{command_def primcorecursive}) target? @{syntax pcr_option}? fixes \\ @'where'
+  (@@{command_def primcorec} | @@{command_def primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where'
     (@{syntax pcr_formula} + '|')
   ;
-  @{syntax_def pcr_option}: '(' 'sequential' | 'exhaustive' ')'
+  @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
   ;
   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
 "}