src/HOL/Analysis/Starlike.thy

--- a/src/HOL/Analysis/Starlike.thy	Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Sat Dec 29 15:43:53 2018 +0100
@@ -5261,7 +5261,7 @@
     qed
     have "\<Inter>{{a. a \<in> K \<and> f a \<in> insert y (range (\<lambda>i. f(X(n + i))))} |n. n \<in> UNIV}
                \<noteq> {}"
-      apply (rule compact_fip_heine_borel)
+      apply (rule compact_fip_Heine_Borel)
        using comf apply force
       using ne  apply (simp add: subset_iff del: insert_iff)
       done