# HG changeset patch
# User blanchet
# Date 1425566677 -3600
# Node ID 63f8527db07fdc53f4fb1057391c40d60f0e5514
# Parent  8273b65620f9a3928d8b923b6f41a6e51fcd5e68
strengthened tactic

diff -r 8273b65620f9 -r 63f8527db07f 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:58:35 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Mar 05 15:44:37 2015 +0100
@@ -119,7 +119,7 @@
             REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
           else
             rtac FalseE THEN'
-            (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
+            (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT o atac ORELSE'
              cut_tac fun_disc') THEN'
             dresolve_tac ctxt distinct_discs THEN' etac notE THEN' atac)
       fun_discss) THEN'