diff -r 82a604715919 -r dc85b5b3a532 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -3720,7 +3720,7 @@
           by (auto simp: algebra_simps)
         have "x \<in> T" "x \<noteq> a" using that by auto
         then have axa: "a + (x - a) \<in> affine hull S"
-           by (metis (no_types) add.commute affS diff_add_cancel set_rev_mp)
+           by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD)
         then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
           using \<open>x \<noteq> a\<close> dd1 by fastforce
         with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"