src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
     m excludesss =
   prelude_tac ctxt defs (fun_sel RS trans) THEN
   cases_tac ctxt k m excludesss THEN
-  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
+  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
     eresolve_tac falseEs ORELSE'
     resolve_tac split_connectI ORELSE'
     Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
     Splitter.split_tac (split_if :: splits) ORELSE'
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
-       sum.cases} @ mapsx @ map_comps @ map_idents)))));
+       sum.cases} @ mapsx @ map_comps @ map_idents))) ORELSE'
+    fo_rtac @{thm cong} ctxt ORELSE'
+    rtac ext));
 
 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
   HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
     (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);