src/HOL/Library/Finite_Map.thy

   "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=)) (\<lambda>f. (\<circ>) (map_option f)) fmmap"
   unfolding fmmap_def
   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]:
   "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=) ===> (=)) rel_map fmrel"
   unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce