diff -r e5995950b98a -r 2562f151541c src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Wed Jul 19 22:56:16 2017 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Thu Jul 20 14:05:29 2017 +0100
@@ -5,7 +5,7 @@
 section \<open>Continuous extensions of functions: Urysohn's lemma, Dugundji extension theorem, Tietze\<close>
 
 theory Continuous_Extension
-imports Convex_Euclidean_Space
+imports Starlike
 begin
 
 subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>