strengthened tactic to handle 'disc_iff' equations of the form '... = False'

--- 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 =