diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Sun Nov 18 18:07:51 2018 +0000
@@ -818,7 +818,7 @@
   by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
 
 lemma fmran'_transfer[transfer_rule]:
-  "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. UNION (range x) set_option) fmran'"
+  "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. \<Union>(set_option ` (range x))) fmran'"
   unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
 
 lemma fmrel_transfer[transfer_rule]: