src/HOL/Analysis/Riemann_Mapping.thy

--- a/src/HOL/Analysis/Riemann_Mapping.thy	Tue Oct 10 14:03:51 2017 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Tue Oct 10 17:15:37 2017 +0100
@@ -1435,7 +1435,7 @@
       then have "S = g ` (ball 0 1)"
         by (force simp:)
       then have "open S"
-        by (metis Topology_Euclidean_Space.open_ball g inj_on_def open_mapping_thm3)
+        by (metis open_ball g inj_on_def open_mapping_thm3)
     }
     with that show "open S" by auto
   qed