--- a/src/HOL/UNITY/ELT.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/ELT.thy Wed Feb 17 21:51:56 2016 +0100
@@ -141,7 +141,6 @@
lemma leadsETo_UN:
"(!!i. i : I ==> F : (A i) leadsTo[CC] B)
==> F : (UN i:I. A i) leadsTo[CC] B"
-apply (subst Union_image_eq [symmetric])
apply (blast intro: leadsETo_Union)
done
@@ -397,7 +396,6 @@
lemma LeadsETo_UN:
"(!!i. i : I ==> F : (A i) LeadsTo[CC] B)
==> F : (UN i:I. A i) LeadsTo[CC] B"
-apply (simp only: Union_image_eq [symmetric])
apply (blast intro: LeadsETo_Union)
done