# HG changeset patch
# User blanchet
# Date 1380206492 -7200
# Node ID 9fc9a59ad579a039ae80256bd5b3e8f302de403f
# Parent  9008c48061983b57c730e5e5cad12c4e4a92d8f7
strengthened tactic

diff -r 9008c4806198 -r 9fc9a59ad579 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 16:25:12 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 16:41:32 2013 +0200
@@ -40,7 +40,7 @@
 fun mk_primcorec_assumption_tac ctxt discIs =
   HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
       @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
-    SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE'
+    SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
     resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
     dresolve_tac discIs THEN' atac)))));