# HG changeset patch
# User blanchet
# Date 1388694921 -3600
# Node ID 790362e13e0d8a106d7e26449d387f0efc8c9ae8
# Parent  a426e38a8a7eb86be0364ff6f1126e49816d6623
made tactic more robust

diff -r a426e38a8a7e -r 790362e13e0d src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 20:51:09 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 21:35:21 2014 +0100
@@ -85,8 +85,8 @@
           if Thm.eq_thm (fun_disc', fun_disc) then
             REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
           else
-            rtac FalseE THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
-            DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac))
+            rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
+            dresolve_tac disc_excludes THEN' etac notE THEN' atac)
       fun_discss) THEN'
     rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);