add 'set_thms' to 'fp_sugar'

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:33:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:33:36 2014 +0200
@@ -21,7 +21,8 @@
      rel_distincts: thm list,
      rel_sels: thm list,
      rel_intros: thm list,
-     rel_cases: thm list}
+     rel_cases: thm list,
+     set_thms: thm list}
 
   type fp_co_induct_sugar =
     {co_rec: term,
@@ -178,7 +179,8 @@
    rel_distincts: thm list,
    rel_sels: thm list,
    rel_intros: thm list,
-   rel_cases: thm list};
+   rel_cases: thm list,
+   set_thms: thm list};
 
 type fp_co_induct_sugar =
   {co_rec: term,
@@ -205,7 +207,7 @@
    fp_co_induct_sugar: fp_co_induct_sugar};
 
 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts,
-    rel_sels, rel_intros, rel_cases} : fp_bnf_sugar) =
+    rel_sels, rel_intros, rel_cases, set_thms} : 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,
@@ -213,7 +215,8 @@
    rel_distincts = map (Morphism.thm phi) rel_distincts,
    rel_sels = map (Morphism.thm phi) rel_sels,
    rel_intros = map (Morphism.thm phi) rel_intros,
-   rel_cases = map (Morphism.thm phi) rel_cases};
+   rel_cases = map (Morphism.thm phi) rel_cases,
+   set_thms = map (Morphism.thm phi) set_thms};
 
 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
     co_rec_discs, co_rec_selss} : fp_co_induct_sugar) =
@@ -297,7 +300,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 map_selss rel_selss rel_intross rel_casess noted =
+    rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -316,7 +319,8 @@
             rel_distincts = nth rel_distinctss kk,
             rel_sels = nth rel_selss kk,
             rel_intros = nth rel_intross kk,
-            rel_cases = nth rel_casess kk},
+            rel_cases = nth rel_casess kk,
+            set_thms = nth set_thmss kk},
          fp_co_induct_sugar =
            {co_rec = nth co_recs kk,
             common_co_inducts = common_co_inducts,
@@ -964,7 +968,7 @@
         map subst rel_sel_thms,
         map subst rel_intro_thms,
         [subst rel_cases_thm],
-        map (map subst) set0_thmss), lthy')
+        map subst set_thms), lthy')
     end;
 
 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list);
@@ -2072,8 +2076,9 @@
         o split_list;
 
     fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
-        rel_distincts setss =
-      injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss;
+        rel_distincts set_thmss =
+      injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @
+      set_thmss;
 
     fun mk_co_rec_transfer_goals lthy co_recs =
       let
@@ -2102,7 +2107,7 @@
 
     fun derive_note_induct_recs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
-            rel_intross, rel_casess, setss),
+            rel_intross, rel_casess, set_thmss),
            (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
@@ -2134,7 +2139,7 @@
             end;
 
         val simp_thmss =
-          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss setss;
+          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (if nn > 1 then
@@ -2160,8 +2165,9 @@
           (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
         |-> 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 map_selss rel_selss rel_intross rel_casess
+          map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
+          (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss
+          rel_intross rel_casess set_thmss
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2181,7 +2187,7 @@
 
     fun derive_note_coinduct_corecs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
-            rel_intross, rel_casess, setss),
+            rel_intross, rel_casess, set_thmss),
            (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
@@ -2243,7 +2249,7 @@
         val simp_thmss =
           map6 mk_simp_thms ctr_sugars
             (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
-            map_thmss rel_injectss rel_distinctss setss;
+            map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (set_inductN, set_induct_thms, nth set_induct_attrss) ::
@@ -2277,7 +2283,7 @@
           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 map_selss rel_selss
-          rel_intross rel_casess
+          rel_intross rel_casess set_thmss
       end;
 
     val lthy'' = lthy'

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 13:33:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 13:33:36 2014 +0200
@@ -294,7 +294,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, map_sels, rel_injects, rel_distincts, rel_sels,
-              rel_intros, rel_cases, ...}, ...} : fp_sugar) =
+              rel_intros, rel_cases, set_thms, ...}, ...} : 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,
@@ -310,7 +310,8 @@
               rel_distincts = rel_distincts,
               rel_sels = rel_sels,
               rel_intros = rel_intros,
-              rel_cases = rel_cases},
+              rel_cases = rel_cases,
+              set_thms = set_thms},
            fp_co_induct_sugar =
              {co_rec = co_rec,
               common_co_inducts = common_co_inducts,

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:33:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:33:36 2014 +0200
@@ -88,7 +88,8 @@
         rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
         rel_sels = [],
         rel_intros = [],
-        rel_cases = []},
+        rel_cases = [],
+        set_thms = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
         common_co_inducts = @{thms sum.induct},
@@ -137,7 +138,8 @@
         rel_distincts = [],
         rel_sels = [],
         rel_intros = [],
-        rel_cases = []},
+        rel_cases = [],
+        set_thms = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
         common_co_inducts = @{thms prod.induct},