diff -r 0d60d2118544 -r c94531b5007d src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Tue Oct 10 14:03:51 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Oct 10 17:15:37 2017 +0100
@@ -6,8 +6,7 @@
 section \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close>
 
 theory Tagged_Division
-imports
-  Topology_Euclidean_Space
+  imports Connected
 begin
 
 term comm_monoid