1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Sep 24 16:59:14 2013 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Sep 24 17:06:06 2013 +0200
     1.3 @@ -2023,10 +2023,10 @@
     1.4  Primitive corecursive definitions have the following general syntax:
     1.5  
     1.6  @{rail "
     1.7 -  (@@{command_def primcorec} | @@{command_def primcorecursive}) target? @{syntax pcr_option}? fixes \\ @'where'
     1.8 +  (@@{command_def primcorec} | @@{command_def primcorecursive}) target? \\ @{syntax pcr_option}? fixes @'where'
     1.9      (@{syntax pcr_formula} + '|')
    1.10    ;
    1.11 -  @{syntax_def pcr_option}: '(' 'sequential' | 'exhaustive' ')'
    1.12 +  @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
    1.13    ;
    1.14    @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
    1.15  "}