# HG changeset patch
# User blanchet
# Date 1389365293 -3600
# Node ID 63a5e0d8ce3bdd071dd8e6b9891e0991296033db
# Parent  b502f04c0442322f875353f0ae418d37d8a53bfe
strengthened tactic to handle 'disc_iff' equations of the form '... = False'

diff -r b502f04c0442 -r 63a5e0d8ce3b src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 15:22:23 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Fri Jan 10 15:48:13 2014 +0100
@@ -118,10 +118,13 @@
           if eq_list Thm.eq_thm (fun_discs', fun_discs) then
             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 THEN'
+            rtac FalseE THEN'
+            (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac ORELSE'
+             cut_tac fun_disc') THEN'
             dresolve_tac disc_excludes THEN' etac notE THEN' atac)
       fun_discss) THEN'
-    resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac);
+    (etac FalseE ORELSE'
+     resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
     m excludesss =