src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML

   | mk_partial_compN n gT fT g =
     let val g' = mk_partial_compN (n - 1) gT (range_type fT) g in
       mk_partial_comp (fastype_of g') fT g'
     end;
 
-fun mk_compN bound_Ts n (g, f) =
+fun mk_compN n bound_Ts (g, f) =
   let val typof = curry fastype_of1 bound_Ts in
     mk_partial_compN n (typof g) (typof f) g $ f
   end;
+
+val mk_comp = mk_compN 1;
 
 fun factor_out_types ctxt massage destU U T =
   (case try destU U of
     SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
   | NONE => invalid_map ctxt);

     permute_like (op aconv) flat_fs fs flat_fs'
   end;
 
 fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
   let
+    fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
+
     val typof = curry fastype_of1 bound_Ts;
     val build_map_fst = build_map ctxt (fst_const o fst);
 
     val yT = typof y;
     val yU = typof y';
 
     fun y_of_y' () = build_map_fst (yU, yT) $ y';
     val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
 
     fun massage_mutual_fun U T t =
-      if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
-      else HOLogic.mk_comp (t, build_map_fst (U, T));
+      (case t of
+        Const (@{const_name comp}, comp_T) $ t1 $ t2 =>
+        mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2)
+      | _ =>
+        if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
+        else mk_comp bound_Ts (t, build_map_fst (U, T)));
 
     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
           SOME (map0, fs) =>
           let

           end
         | NONE => raise AINT_NO_MAP t)
       | massage_map _ _ t = raise AINT_NO_MAP t
     and massage_map_or_map_arg U T t =
       if T = U then
-        if has_call t then unexpected_rec_call ctxt t else t
+        tap check_no_call t
       else
         massage_map U T t
         handle AINT_NO_MAP _ => massage_mutual_fun U T t;
 
     fun massage_call (t as t1 $ t2) =

             handle AINT_NO_MAP t' => invalid_map ctxt t'
           else
             let val (g, xs) = Term.strip_comb t2 in
               if g = y then
                 if exists has_call xs then unexpected_rec_call ctxt t2
-                else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
+                else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs)
               else
                 ill_formed_rec_call ctxt t
             end
         else
           elim_y t

       else build_map_Inl (T, U) $ t;
 
     fun massage_mutual_fun bound_Ts U T t =
       (case t of
         Const (@{const_name comp}, comp_T) $ t1 $ t2 =>
-        mk_compN bound_Ts 1 (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
+        mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
       | _ =>
         let
           val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
             domain_type (fastype_of1 (bound_Ts, t)));
         in