src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML

   end;
 
 fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
   let
     val typof = curry fastype_of1 bound_Ts;
-    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o fst);
+    val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
 
     fun check_and_massage_direct_call U T t =
       if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
-      else build_map_Inl (U, T) $ t;
+      else build_map_Inl (T, U) $ t;
 
     fun check_and_massage_unapplied_direct_call U T t =
       let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
         Term.lambda var (check_and_massage_direct_call U T (t $ var))
       end;

                   list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
                 end
               | NONE =>
                 (case t of
                   t1 $ t2 =>
-                  if has_call t2 then
+                  (if has_call t2 then
                     check_and_massage_direct_call U T t
                   else
                     massage_map U T t1 $ t2
-                    handle AINT_NO_MAP _ => check_and_massage_direct_call U T t
+                    handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
                 | _ => check_and_massage_direct_call U T t))
             | _ => ill_formed_corec_call ctxt t))
         U T
   in
     massage_call res_U (typof t) (Envir.beta_eta_contract t)