diff -r dc746d43f40e -r a4abec71279a src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Feb 28 13:51:47 2017 +0000
@@ -1330,7 +1330,7 @@
     shows "g1 x = g2 x"
 proof -
   have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
-  def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}"
+  define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
   have "connected U" by (rule in_components_connected [OF u_compt])
   have contu: "continuous_on U g1" "continuous_on U g2"
        using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+