src/HOL/Analysis/Tagged_Division.thy

--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 07 13:08:50 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 07 13:16:33 2019 +0100
@@ -6,7 +6,7 @@
 section%important \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
 (*FIXME move together with Henstock_Kurzweil_Integration.thy  *)
 theory Tagged_Division
-  imports Connected
+  imports Topology_Euclidean_Space
 begin
 
 term comm_monoid