--- a/src/HOL/Analysis/Path_Connected.thy Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Sun Dec 01 19:10:57 2019 +0000
@@ -4003,4 +4003,5 @@
shows "\<exists>g. homeomorphism S T f g"
using assms injective_into_1d_eq_homeomorphism by blast
+
end