--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 05 18:19:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 05 23:30:02 2014 +0100
@@ -130,7 +130,7 @@
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'
@@ -138,7 +138,9 @@
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'