changed syntax of map: and rel: arguments to BNF-based datatypes

--- 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>}

--- a/src/HOL/BNF_Examples/ListF.thy	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/BNF_Examples/ListF.thy	Tue Jun 10 21:15:57 2014 +0200
@@ -12,9 +12,12 @@
 imports Main
 begin
 
-datatype_new 'a listF (map: mapF rel: relF) =
+datatype_new 'a listF =
     NilF
   | Conss (hdF: 'a) (tlF: "'a listF")
+for
+  map: mapF
+  rel: relF
 where
   "tlF NilF = NilF"
 

--- a/src/HOL/BNF_Examples/Stream.thy	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream.thy	Tue Jun 10 21:15:57 2014 +0200
@@ -12,8 +12,11 @@
 imports "~~/src/HOL/Library/Nat_Bijection"
 begin
 
-codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
+codatatype (sset: 'a) stream =
   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+for
+  map: smap
+  rel: stream_all2
 
 (*for code generation only*)
 definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where

--- a/src/HOL/BNF_Examples/Stream_Processor.thy	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Tue Jun 10 21:15:57 2014 +0200
@@ -150,7 +150,7 @@
 
 section {* Generalization to an Arbitrary BNF as Codomain *}
 
-bnf_axiomatization ('a, 'b) F (map: F)
+bnf_axiomatization ('a, 'b) F for map: F
 
 notation BNF_Def.convol ("<_ , _>")
 

--- a/src/HOL/Library/bnf_axiomatization.ML	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Tue Jun 10 21:15:57 2014 +0200
@@ -108,13 +108,13 @@
   @{keyword "]"} || Scan.succeed [];
 
 val parse_bnf_axiomatization =
-  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
-    parse_witTs -- Parse.opt_mixfix;
+  parse_type_args_named_constrained -- Parse.binding -- parse_witTs -- Parse.opt_mixfix --
+  parse_map_rel_bindings;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
     (parse_bnf_axiomatization >> 
-      (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
+      (fn ((((bsTs, b), witTs), mx), (mapb, relb)) =>
          bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd));
 
 end;

--- a/src/HOL/List.thy	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/List.thy	Tue Jun 10 21:15:57 2014 +0200
@@ -8,9 +8,12 @@
 imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
 begin
 
-datatype_new (set: 'a) list  (map: map rel: list_all2) =
+datatype_new (set: 'a) list =
     Nil  ("[]")
   | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
+for
+  map: map
+  rel: list_all2
 where
   "tl [] = []"
 

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jun 10 21:15:57 2014 +0200
@@ -72,8 +72,9 @@
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
     (bool * bool)
-    * ((((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
-       * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * term list) list ->
+    * ((((((binding option * (typ * sort)) list * binding) * mixfix)
+         * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding))
+       * term list) list ->
     local_theory -> local_theory
   val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -245,16 +246,12 @@
   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
   handle THM _ => thm;
 
-type co_datatype_spec =
-  (((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
-   * ((binding, binding * typ) ctr_spec * mixfix) list) * term list;
-
 fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
 fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
-fun map_binding_of_spec ((((_, (b, _)), _), _), _) = b;
-fun rel_binding_of_spec ((((_, (_, b)), _), _), _) = b;
-fun mixfix_of_spec (((_, mx), _), _) = mx;
-fun mixfixed_ctr_specs_of_spec ((_, mx_ctr_specs), _) = mx_ctr_specs;
+fun mixfix_of_spec ((((_, mx), _), _), _) = mx;
+fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs;
+fun map_binding_of_spec ((_, (b, _)), _) = b;
+fun rel_binding_of_spec ((_, (_, b)), _) = b;
 fun sel_default_eqs_of_spec (_, ts) = ts;
 
 fun add_nesty_bnf_names Us =
@@ -1547,8 +1544,8 @@
   Parse.enum1 "|" (parse_ctr_spec Parse.binding parse_ctr_arg -- Parse.opt_mixfix);
 
 val parse_spec =
-  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
-  Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs) -- parse_sel_default_eqs;
+  parse_type_args_named_constrained -- Parse.binding -- Parse.opt_mixfix --
+  (@{keyword "="} |-- parse_ctr_specs) -- parse_map_rel_bindings -- parse_sel_default_eqs;
 
 val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
 

--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue Jun 10 19:51:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Jun 10 21:15:57 2014 +0200
@@ -308,9 +308,9 @@
   | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
 
 val parse_map_rel_bindings =
-  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
-    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
-  Scan.succeed no_map_rel;
+  @{keyword "for"} |-- Scan.repeat parse_map_rel_binding
+    >> (fn ps => fold extract_map_rel ps no_map_rel)
+  || Scan.succeed no_map_rel;
 
 
 (*TODO: is this really different from Typedef.add_typedef_global?*)