src/HOL/Analysis/Connected.thy

--- a/src/HOL/Analysis/Connected.thy	Sat Dec 29 18:40:29 2018 +0000
+++ b/src/HOL/Analysis/Connected.thy	Sat Dec 29 20:32:09 2018 +0100
@@ -5,7 +5,9 @@
 section \<open>Connected Components, Homeomorphisms, Baire property, etc\<close>
 
 theory Connected
-imports Topology_Euclidean_Space
+  imports
+    "HOL-Library.Indicator_Function"
+    Topology_Euclidean_Space
 begin
 
 subsection%unimportant \<open>More properties of closed balls, spheres, etc\<close>