--- a/Max.thy	Thu Sep 21 14:33:13 2017 +0100
+++ b/Max.thy	Fri Sep 22 03:08:30 2017 +0100
@@ -128,10 +128,11 @@
   using assms[simp]
 proof -
   have "?L = Max (\<Union>(f ` A))"
-    by (fold Union_image_eq, simp)
+    by simp
   also have "... = ?R"
     by (subst Max_Union, simp+)
-  finally show ?thesis .
+  finally show ?thesis
+    using \<open>Max (UNION A f) = Max (Max ` f ` A)\<close> by blast
 qed
 
 lemma max_Max_eq: