diff -r 1cf129590be8 -r 24106dc44def src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 17 21:51:56 2016 +0100
@@ -540,8 +540,8 @@
 fun mk_ctor_set_tac ctxt set set_map set_maps =
   let
     val n = length set_maps;
-    fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
-      rtac ctxt @{thm Union_image_eq};
+    fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans)
+      THEN' rtac ctxt @{thm refl};
   in
     EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong,
       rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]),