src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

      co_rec_disc_iffs: thm list,
      co_rec_selss: thm list list,
      co_rec_codes: thm list,
      co_rec_transfers: thm list,
      common_rel_co_inducts: thm list,
-     rel_co_inducts: thm list}
+     rel_co_inducts: thm list,
+     common_set_inducts: thm list}
 
   type fp_sugar =
     {T: typ,
      BT: typ,
      X: typ,

    co_rec_disc_iffs: thm list,
    co_rec_selss: thm list list,
    co_rec_codes: thm list,
    co_rec_transfers: thm list,
    common_rel_co_inducts: thm list,
-   rel_co_inducts: thm list};
+   rel_co_inducts: thm list,
+   common_set_inducts: thm list};
 
 type fp_sugar =
   {T: typ,
    BT: typ,
    X: typ,

    set_intros = map (Morphism.thm phi) set_intros,
    set_cases = map (Morphism.thm phi) set_cases};
 
 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_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers,
-    common_rel_co_inducts, rel_co_inducts} : fp_co_induct_sugar) =
+    common_rel_co_inducts, rel_co_inducts, common_set_inducts} : fp_co_induct_sugar) =
   {co_rec = Morphism.term phi co_rec,
    common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    co_inducts = map (Morphism.thm phi) co_inducts,
    co_rec_def = Morphism.thm phi co_rec_def,
    co_rec_thms = map (Morphism.thm phi) co_rec_thms,

    co_rec_disc_iffs = map (Morphism.thm phi) co_rec_disc_iffs,
    co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
    co_rec_codes = map (Morphism.thm phi) co_rec_codes,
    co_rec_transfers = map (Morphism.thm phi) co_rec_transfers,
    common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts,
-   rel_co_inducts = map (Morphism.thm phi) rel_co_inducts};
+   rel_co_inducts = map (Morphism.thm phi) rel_co_inducts,
+   common_set_inducts = map (Morphism.thm phi) common_set_inducts};
 
 fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, case_transfers,
     disc_transfers} : fp_ctr_sugar) =
   {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    ctr_defs = map (Morphism.thm phi) ctr_defs,

 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 set_thmss set_selss
     set_intross set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
-    co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss noted =
+    co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
         {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
          pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,

             co_rec_disc_iffs = nth co_rec_disc_iffss kk,
             co_rec_selss = nth co_rec_selsss kk,
             co_rec_codes = nth co_rec_codess kk,
             co_rec_transfers = nth co_rec_transferss kk,
             common_rel_co_inducts = common_rel_co_inducts,
-            rel_co_inducts = nth rel_co_inductss kk}}
+            rel_co_inducts = nth rel_co_inductss kk,
+            common_set_inducts = common_set_inducts}}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
     register_fp_sugars_raw fp_sugars
     #> fold (interpret_bnf plugins) (#bnfs fp_res)
     #> interpret_fp_sugars plugins fp_sugars

           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 set_thmss set_selss set_intross set_casess ctr_transferss
           case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
-          common_rel_induct_thms rel_induct_thmss
+          common_rel_induct_thms rel_induct_thmss []
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
       let
         val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs;

           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 set_thmss set_selss set_intross set_casess ctr_transferss
           case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
-          corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss
+          corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
       end;
 
     val lthy'' = lthy'
       |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
       |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~