src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

             val sumEN_thm' =
               Local_Defs.unfold lthy @{thms all_unit_eq}
                 (Drule.instantiate' (map (SOME o certifyT lthy) prod_Ts) [] (mk_sumEN n))
               |> Morphism.thm phi;
           in
-            mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm'
+            mk_exhaust_tac ctxt n ctr_defs fld_iff_unf_thm sumEN_thm'
           end;
 
         val inject_tacss =
           map2 (fn 0 => K []
                  | _ => fn ctr_def => [fn {context = ctxt, ...} =>