add 'map_sels' to 'fp_sugar'

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:32:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:32:53 2014 +0200
@@ -16,6 +16,7 @@
   type fp_bnf_sugar =
     {map_thms: thm list,
      map_disc_iffs: thm list,
+     map_sels: thm list,
      rel_injects: thm list,
      rel_distincts: thm list}
 
@@ -169,6 +170,7 @@
 type fp_bnf_sugar =
   {map_thms: thm list,
    map_disc_iffs: thm list,
+   map_sels: thm list,
    rel_injects: thm list,
    rel_distincts: thm list};
 
@@ -196,9 +198,10 @@
    fp_bnf_sugar: fp_bnf_sugar,
    fp_co_induct_sugar: fp_co_induct_sugar};
 
-fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, rel_injects, rel_distincts} : fp_bnf_sugar) =
+fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts} : fp_bnf_sugar) =
   {map_thms = map (Morphism.thm phi) map_thms,
    map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
+   map_sels = map (Morphism.thm phi) map_sels,
    rel_injects = map (Morphism.thm phi) rel_injects,
    rel_distincts = map (Morphism.thm phi) rel_distincts};
 
@@ -284,7 +287,7 @@
 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
     live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss
     common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
-    rel_distinctss map_disc_iffss noted =
+    rel_distinctss map_disc_iffss map_selss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -298,6 +301,7 @@
          fp_bnf_sugar =
            {map_thms = nth map_thmss kk,
             map_disc_iffs = nth map_disc_iffss kk,
+            map_sels = nth map_selss kk,
             rel_injects = nth rel_injectss kk,
             rel_distincts = nth rel_distinctss kk},
          fp_co_induct_sugar =
@@ -459,7 +463,7 @@
       distincts, distinct_discsss, ...} : ctr_sugar)
     lthy =
   if live = 0 then
-    (([], [], [], [], []), lthy)
+    (([], [], [], [], [], []), lthy)
   else
     let
       val n = length ctr_Tss;
@@ -939,8 +943,12 @@
 
       val subst = Morphism.thm (substitute_noted_thm noted);
     in
-      ((map subst map_thms, map subst map_disc_iff_thms, map subst rel_inject_thms,
-        map subst rel_distinct_thms, map (map subst) set0_thmss), lthy')
+      ((map subst map_thms,
+        map subst map_disc_iff_thms,
+        map subst map_sel_thms,
+        map subst rel_inject_thms,
+        map subst rel_distinct_thms,
+        map (map subst) set0_thmss), lthy')
     end;
 
 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list);
@@ -2044,7 +2052,7 @@
 
     fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
       fold_map I wrap_one_etc lthy
-      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list5 o split_list)
+      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list6 o split_list)
         o split_list;
 
     fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2077,7 +2085,7 @@
       end;
 
     fun derive_note_induct_recs_thms_for_types
-        ((((map_thmss, map_disc_iffss, rel_injectss, rel_distinctss, setss),
+        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, setss),
            (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
@@ -2136,7 +2144,7 @@
         |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
           map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
-          rel_injectss rel_distinctss map_disc_iffss
+          rel_injectss rel_distinctss map_disc_iffss map_selss
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2155,7 +2163,7 @@
       end;
 
     fun derive_note_coinduct_corecs_thms_for_types
-        ((((map_thmss, map_disc_iffss, rel_injectss, rel_distinctss, setss),
+        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, setss),
            (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
@@ -2250,7 +2258,7 @@
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
           map_thmss [coinduct_thm, coinduct_strong_thm]
           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
-          corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss
+          corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss
       end;
 
     val lthy'' = lthy'

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 13:32:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 13:32:53 2014 +0200
@@ -293,7 +293,7 @@
 
         fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
             co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
-            ({fp_bnf_sugar = {map_disc_iffs, rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
+            ({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
            pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
            live_nesting_bnfs = live_nesting_bnfs,
@@ -304,6 +304,7 @@
            fp_bnf_sugar =
              {map_thms = map_thms,
               map_disc_iffs = map_disc_iffs,
+              map_sels = map_sels,
               rel_injects = rel_injects,
               rel_distincts = rel_distincts},
            fp_co_induct_sugar =

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:32:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:32:53 2014 +0200
@@ -83,6 +83,7 @@
      fp_bnf_sugar =
        {map_thms = @{thms map_sum.simps},
         map_disc_iffs = [],
+        map_sels = [],
         rel_injects = @{thms rel_sum_simps(1,4)},
         rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
      fp_co_induct_sugar =
@@ -128,6 +129,7 @@
      fp_bnf_sugar =
        {map_thms = @{thms map_prod_simp},
         map_disc_iffs = [],
+        map_sels = [],
         rel_injects = @{thms rel_prod_apply},
         rel_distincts = []},
      fp_co_induct_sugar =

--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 06 13:32:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 06 13:32:53 2014 +0200
@@ -59,6 +59,8 @@
     'i list -> 'j -> 'k list * 'j
   val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list
+  val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list *
+    'e list * 'f list
 
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_Freesss: string -> typ list list list -> Proof.context ->
@@ -294,6 +296,11 @@
     let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
 
+fun split_list6 [] = ([], [], [], [], [], [])
+  | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end;
+
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);