diff -r 210b687cdbbe -r 9ca183045102 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:37 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:39 2018 +0000
@@ -1355,7 +1355,7 @@
     proof safe
       fix i :: 'a
       assume i: "i \<in> Basis"
-      have "norm (x - y) < MINIMUM Basis ((\<bullet>) x)"
+      have "norm (x - y) < Min (((\<bullet>) x) ` Basis)"
         using y by (auto simp: dist_norm less_eq_real_def)
       also have "... \<le> x\<bullet>i"
         using i by auto