src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

      xxfold_thmss: thm list list,
      xxrec_thmss: thm list list};
 
   val fp_sugar_of: local_theory -> string -> fp_sugar option
 
-  val build_maps: local_theory -> typ list -> (int -> typ * typ -> term) -> typ * typ -> term
+  val build_map: local_theory -> typ list -> (int -> typ * typ -> term) -> typ * typ -> term
 
   val mk_fp_iter_fun_types: term -> typ list
   val mk_fun_arg_typess: int -> int list -> typ -> typ list list
   val unzip_recT: typ list -> typ -> typ list * typ list
   val mk_fold_fun_typess: typ list list list -> typ list list -> typ list list

     val live = live_of_bnf bnf;
     val mapx = mk_map live Ts Us (map_of_bnf bnf);
     val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
   in Term.list_comb (mapx, map build_arg TUs') end;
 
-fun build_maps lthy Ts build_simple =
+fun build_map lthy Ts build_simple =
   let
     fun build (TU as (T, U)) =
       if T = U then
         id_const T
       else
         (case find_index (curry (op =) T) Ts of
           ~1 => build_map_step lthy build TU
         | kk => build_simple kk TU);
+  in build end;
+
+fun build_map' lthy build_simple =
+  let
+    fun build (TU as (T, U)) =
+      if T = U then
+        id_const T
+      else
+        (case TU of
+          (Type (s, _), Type (s', _)) =>
+          if s = s' then build_map_step lthy build TU else build_simple TU
+        | _ => build_simple TU);
   in build end;
 
 fun build_rel_step lthy build_arg (Type (s, Ts)) =
   let
     val bnf = the (bnf_of lthy s);

 
         val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
 
         fun unzip_iters fiters combine (x as Free (_, T)) =
           if exists_subtype_in fpTs T then
-            combine (x, build_maps lthy fpTs (K o nth fiters) (T, mk_U T) $ x)
+            combine (x, build_map lthy fpTs (K o nth fiters) (T, mk_U T) $ x)
           else
             ([x], []);
 
         val gxsss = map (map (flat_rec (unzip_iters gfolds (fn (_, t) => ([t], []))))) xsss;
         val hxsss = map (map (flat_rec (unzip_iters hrecs (pairself single)))) xsss;

 
         val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs);
 
         fun intr_coiters fcoiters [] [cf] =
             let val T = fastype_of cf in
-              if exists_subtype_in Cs T then build_maps lthy Cs (K o nth fcoiters) (T, mk_U T) $ cf
+              if exists_subtype_in Cs T then build_map lthy Cs (K o nth fcoiters) (T, mk_U T) $ cf
               else cf
             end
           | intr_coiters fcoiters [cq] [cf, cf'] =
             mk_If cq (intr_coiters fcoiters [] [cf]) (intr_coiters fcoiters [] [cf']);
 

 
         fun define_fold_rec no_defs_lthy =
           let
             val fpT_to_C = fpT --> C;
 
-            fun build_prod_proj mk_proj (TU as (T, U)) =
-              if T = U then
-                id_const T
-              else
-                (case TU of
-                  (Type (s, _), Type (s', _)) =>
-                  if s = s' then build_map_step lthy (build_prod_proj mk_proj) TU else mk_proj T
-                | _ => mk_proj T);
+            fun build_prod_proj mk_proj = build_map' lthy (mk_proj o fst);
 
             (* TODO: Avoid these complications; cf. corec case *)
             fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
                 if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
               | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)

 
         fun define_unfold_corec no_defs_lthy =
           let
             val B_to_fpT = C --> fpT;
 
-            fun build_sum_inj mk_inj (TU as (T, U)) =
-              if T = U then
-                id_const T
-              else
-                (case TU of
-                  (Type (s, _), Type (s', _)) =>
-                  if s = s' then build_map_step lthy (build_sum_inj mk_inj) TU
-                  else uncurry mk_inj (dest_sumT U)
-                | _ => uncurry mk_inj (dest_sumT U));
+            fun build_sum_inj mk_inj = build_map' lthy (uncurry mk_inj o dest_sumT o snd);
 
             fun build_dtor_coiter_arg _ [] [cf] = cf
               | build_dtor_coiter_arg T [cq] [cf, cf'] =
                 mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
                   (build_sum_inj Inr_const (fastype_of cf', T) $ cf')