diff -r 1d9a96750a40 -r a043de9ad41e src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -3604,7 +3604,7 @@
   obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
 proof (cases "S = {} \<or> T = {}")
   case True with assms that show ?thesis
-    by (auto simp: intro: ANR_imp_neighbourhood_retract)
+    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
 next
   case False
   then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto