src/HOL/Tools/BNF/bnf_fp_util.ML

     val map_cong_active_args1 = replicate n (if is_rec
       then fp_case fp @{thm convol_o} @{thm o_case_sum} RS fun_cong
       else refl);
     val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
     val map_cong_active_args2 = replicate n (if is_rec
-      then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_sum_map_id}
+      then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_map_sum_id}
       else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
     fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
     val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
     val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;