src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

     val fp_b_names = map base_name_of_typ fpTs;
 
     val ctor_fold_fun_Ts = mk_fp_iter_fun_types (hd ctor_folds);
     val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs);
 
-    val (((_, y_Tssss, gss, _), (_, z_Tssss, hss, _)), names_lthy0) =
+    val ((fold_only, rec_only), names_lthy0) =
       mk_fold_rec_args_types Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
 
     val ((((ps, ps'), xsss), us'), names_lthy) =
       names_lthy0
       |> mk_Frees' "P" (map mk_pred1T fpTs)

     val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
     val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
 
     val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
 
-    fun mk_iter_thmss x_Tssss fss iters iter_defs ctor_iter_thms =
+    fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_thms =
       let
         val fiters = map (lists_bmoc fss) iters;
 
         fun mk_goal fss fiter xctr f xs fxs =
           fold_rev (fold_rev Logic.all) (xs :: fss)

             build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
               (fn kk => fn TU => maybe_tick TU (nth us kk) (nth fiters kk))) (T, U) $ x);
 
         val fxsss = map2 (map2 (flat_rec oo map2 unzip_iters)) xsss x_Tssss;
 
-        val goalss = map5 (map4 o mk_goal gss) fiters xctrss fss xsss fxsss;
+        val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
 
         val tacss =
           map2 (map o mk_iter_tac pre_map_defs (nested_map_ids'' @ nesting_map_ids'') iter_defs)
             ctor_iter_thms ctr_defss;
 

           |> Thm.close_derivation;
       in
         map2 (map2 prove) goalss tacss
       end;
 
-    val fold_thmss = mk_iter_thmss y_Tssss gss folds fold_defs ctor_fold_thms;
-    val rec_thmss = mk_iter_thmss z_Tssss hss recs rec_defs ctor_rec_thms;
+    val fold_thmss = mk_iter_thmss fold_only folds fold_defs ctor_fold_thms;
+    val rec_thmss = mk_iter_thmss rec_only recs rec_defs ctor_rec_thms;
   in
     ((induct_thm, induct_thms, [induct_case_names_attr]),
      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
   end;