diff -r f075640b8868 -r 3abf6a722518 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -980,7 +980,7 @@
     proof -
       have f0: "(f \<longlongrightarrow> 0) at_infinity"
       proof -
-        have DIM_complex[intro]: "2 \<le> DIM(complex)"  \<comment>\<open>should not be necessary!\<close>
+        have DIM_complex[intro]: "2 \<le> DIM(complex)"  \<comment> \<open>should not be necessary!\<close>
           by simp
         have "continuous_on (inverse ` (ball 0 r - {0})) f"
           using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast