src/Doc/Datatypes/Datatypes.thy

--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jun 10 21:15:57 2014 +0200
@@ -374,9 +374,12 @@
 
     context early begin
 (*>*)
-    datatype_new (set: 'a) list (map: map rel: list_all2) =
+    datatype_new (set: 'a) list =
       null: Nil
     | Cons (hd: 'a) (tl: "'a list")
+    for
+      map: map
+      rel: list_all2
     where
       "tl Nil = Nil"
 
@@ -440,9 +443,12 @@
 
 text {* \blankline *}
 
-    datatype_new (set: 'a) list (map: map rel: list_all2) =
+    datatype_new (set: 'a) list =
       null: Nil ("[]")
     | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
+    for
+      map: map
+      rel: list_all2
 
 text {*
 \noindent
@@ -472,10 +478,12 @@
 
 @{rail \<open>
   @@{command datatype_new} target? @{syntax dt_options}? \<newline>
-    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') \<newline>
-    (@'where' (@{syntax prop} + '|'))?
+    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
+     @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
   ;
   @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
+  ;
+  @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
 \<close>}
 
 \medskip
@@ -513,11 +521,9 @@
 define, its type parameters, and additional information:
 
 @{rail \<open>
-  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
+  @{syntax_def dt_name}: @{syntax tyargs}? name mixfix?
   ;
   @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')'
-  ;
-  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
 \<close>}
 
 \medskip
@@ -620,7 +626,7 @@
 \end{itemize}
 
 An alternative to @{command datatype_compat} is to use the old package's
-\keyw{rep\_datatype} command. The associated proof obligations must then be
+\keyw{rep\_\allowbreak datatype} command. The associated proof obligations must then be
 discharged manually.
 *}
 
@@ -1555,9 +1561,12 @@
 definition of lazy lists:
 *}
 
-    codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
+    codatatype (lset: 'a) llist =
       lnull: LNil
     | LCons (lhd: 'a) (ltl: "'a llist")
+    for
+      map: lmap
+      rel: llist_all2
     where
       "ltl LNil = LNil"
 
@@ -1568,8 +1577,11 @@
 infinite streams:
 *}
 
-    codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
+    codatatype (sset: 'a) stream =
       SCons (shd: 'a) (stl: "'a stream")
+    for
+      map: smap
+      rel: stream_all2
 
 text {*
 \noindent
@@ -2559,8 +2571,8 @@
 \end{matharray}
 
 @{rail \<open>
-  @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
-    @{syntax wit_types}? mixfix?
+  @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax wit_types}? \<newline>
+    mixfix? @{syntax map_rel}?
   ;
   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
 \<close>}
@@ -2648,7 +2660,7 @@
 @{rail \<open>
   @@{command free_constructors} target? @{syntax dt_options} \<newline>
     name 'for' (@{syntax fc_ctor} + '|') \<newline>
-  (@'where' (@{syntax prop} + '|'))?
+  (@'where' (prop + '|'))?
   ;
   @{syntax_def fc_ctor}: (name ':')? term (name * )
 \<close>}