# HG changeset patch
# User blanchet
# Date 1473693035 -7200
# Node ID e90f51b20215c676a45a78a867b1803dbc13ddfe
# Parent  d0e8921da31193948a0b8abc2cbc8b2f97e608c3
strengthened tactic

diff -r d0e8921da311 -r e90f51b20215 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 12 16:51:55 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 12 17:10:35 2016 +0200
@@ -500,7 +500,7 @@
   ALLGOALS (subst_tac ctxt NONE fp_sets) THEN
   unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_nesting_set_maps @
     live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @
-    @{thms UN_UN_flatten UN_Un sup_assoc[THEN sym]}) THEN
+    @{thms UN_UN_flatten UN_Un_distrib UN_Un sup_assoc[THEN sym]}) THEN
   ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN
   ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN
   ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt);