diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Lifting_Set.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -134,8 +134,8 @@
   "((A ===> B) ===> rel_set A ===> rel_set B) image image"
   unfolding rel_fun_def rel_set_def by simp fast
 
-lemma UNION_transfer [transfer_rule]:
-  "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
+lemma UNION_transfer [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+  "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) (\<lambda>A f. \<Union>(f ` A)) (\<lambda>A f. \<Union>(f ` A))"
   by transfer_prover
 
 lemma Ball_transfer [transfer_rule]:
@@ -172,12 +172,12 @@
   "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind"
   unfolding bind_UNION [abs_def] by transfer_prover
 
-lemma INF_parametric [transfer_rule]:
-  "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
+lemma INF_parametric [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+  "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) (\<lambda>A f. Inf (f ` A)) (\<lambda>A f. Inf (f ` A))"
   by transfer_prover
 
-lemma SUP_parametric [transfer_rule]:
-  "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
+lemma SUP_parametric [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+  "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) (\<lambda>A f. Sup (f ` A)) (\<lambda>A f. Sup (f ` A))"
   by transfer_prover
 
 
@@ -316,7 +316,7 @@
 
 lemma rel_set_UNION:
   assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
-  shows "rel_set R (UNION A f) (UNION B g)"
+  shows "rel_set R (\<Union>(f ` A)) (\<Union>(g ` B))"
   by transfer_prover
 
 end