--- 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);