# HG changeset patch
# User blanchet
# Date 1380663362 -7200
# Node ID bd2e127389f2556e002475a05c25ef3548ecf50c
# Parent  769fcbdf2918095296ef84a8ba4dab7692d034d1
strengthened tactic for right-hand sides involving lambdas

diff -r 769fcbdf2918 -r bd2e127389f2 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Oct 01 22:50:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Oct 01 23:36:02 2013 +0200
@@ -71,14 +71,14 @@
     exclsss =
   mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
   mk_primcorec_cases_tac ctxt k m exclsss THEN
-  unfold_thms_tac ctxt (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @
-    map_idents) THEN
-  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
+  unfold_thms_tac ctxt (@{thms id_apply o_def split_def} @ maps @ map_comps @ map_idents) THEN
+  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext 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'
+    (CHANGED o SELECT_GOAL (unfold_tac @{thms sum.cases} ctxt)) ORELSE'
     etac notE THEN' atac));
 
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =