(case U of

           (case t of

             Type (s, Us) =>

             Const (@{const_name prod_case}, _) $ t' =>

             (case try (dest_ctr ctxt s) t of

             let

               SOME (f, args) =>

               val U' = curried_type U;

               let

               val T' = curried_type T;

                 val typof = curry fastype_of1 bound_Ts;

             in

                 val f' = mk_ctr Us f

               Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'

                 val f'_T = typof f';

             end

                 val arg_Ts = map typof args;

           | t1 $ t2 =>

               in

             (if has_call t2 then

                 Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)

               massage_mutual_call bound_Ts U T t

               end

             else

             | NONE =>

               massage_map bound_Ts U T t1 $ t2

               (case t of

               handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)

                 Const (@{const_name prod_case}, _) $ t' =>

           | Abs (s, T', t') =>

                 let

             Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')

                   val U' = curried_type U;

           | _ => massage_mutual_call bound_Ts U T t)

                   val T' = curried_type T;

                 in

                   Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'

                 end

               | t1 $ t2 =>

                 (if has_call t2 then

                   massage_mutual_call bound_Ts U T t

                 else

                   massage_map bound_Ts U T t1 $ t2

                   handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)

               | Abs (s, T', t') =>

                 Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')

               | _ => massage_mutual_call bound_Ts U T t))

           | _ => ill_formed_corec_call ctxt t)