# HG changeset patch
# User blanchet
# Date 1425563915 -3600
# Node ID 8273b65620f9a3928d8b923b6f41a6e51fcd5e68
# Parent  7892ffd1c39d691681f81d8f4961a6eb380e0f72
strengthened tactic

diff -r 7892ffd1c39d -r 8273b65620f9 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Mar 05 14:25:45 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Mar 05 14:58:35 2015 +0100
@@ -141,7 +141,8 @@
          sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
        mapsx @ map_ident0s @ map_comps))) ORELSE'
     fo_rtac @{thm cong} ctxt ORELSE'
-    rtac @{thm ext}));
+    rtac @{thm ext} ORELSE'
+    mk_primcorec_assumption_tac ctxt []));
 
 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'