src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

     val mss = map (map length) ctr_Tsss;
     val Css = map2 replicate ns Cs;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
+    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
 
     val (_, ctor_fold_fun_Ts) = mk_fp_rec_like true As Cs ctor_folds0;
     val (_, ctor_rec_fun_Ts) = mk_fp_rec_like true As Cs ctor_recs0;

   let
     val nn = length pre_bnfs;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
+    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
+    val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
     val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs;
     val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
-    val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
 
     val (_, dtor_unfold_fun_Ts) = mk_fp_rec_like false As Cs dtor_unfolds0;
     val (_, dtor_corec_fun_Ts) = mk_fp_rec_like false As Cs dtor_corecs0;

       lthy
       |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
       ||>> Variable.variant_fixes fp_b_names
       ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
 
-    val (p_Tss, (r_Tssss, g_sum_prod_Ts, g_Tsss, g_Tssss, pg_Tss),
-         (s_Tssss, h_sum_prod_Ts, h_Tsss, h_Tssss, ph_Tss)) =
+    val (p_Tss, (r_Tssss, _, _, g_Tssss, _), (s_Tssss, _, _, h_Tssss, _)) =
       mk_unfold_corec_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts;
 
     val ((cs, pss, (gssss, rssss), (hssss, sssss)), names_lthy) =
       mk_unfold_corec_vars Cs p_Tss g_Tssss r_Tssss h_Tssss s_Tssss names_lthy;
 

     val nested_bnfs = nesty_bnfs Xs;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
+    val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
-    val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
 
     val live = live_of_bnf any_fp_bnf;
 
     val Bs =
       map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)

 
     val (fp_folds, fp_fold_fun_Ts) = mk_fp_rec_like lfp As Cs fp_folds0;
     val (fp_recs, fp_rec_fun_Ts) = mk_fp_rec_like lfp As Cs fp_recs0;
 
     val (((fold_only, rec_only),
-          (cs, cpss, unfold_only as ((pgss, crssss, cgssss), (_, g_Tsss, _)),
-           corec_only as ((phss, csssss, chssss), (_, h_Tsss, _)))), names_lthy0) =
+          (cs, cpss, unfold_only as ((_, crssss, cgssss), (_, g_Tsss, _)),
+           corec_only as ((_, csssss, chssss), (_, h_Tsss, _)))), _) =
       if lfp then
         let
           val y_Tsss = map3 mk_rec_like_fun_arg_typess ns mss fp_fold_fun_Ts;
           val g_Tss = mk_fold_fun_typess y_Tsss Css;
 

              (rec_thmss, rec_attrs)) =
           derive_induct_fold_rec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct fp_fold_thms
             fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As ctrss ctr_defss folds recs fold_defs
             rec_defs lthy;
 
-        fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
+        val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
         val simp_thmss = mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss;
 
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])

              (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
           derive_coinduct_unfold_corec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct
             fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
             kss mss ns ctrss ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy;
 
-        fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));
+        val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
         fun flat_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
           corec_likes @ disc_corec_likes @ sel_corec_likes;
 
         val simp_thmss =