--- a/src/HOL/Analysis/Homeomorphism.thy Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu May 03 16:17:44 2018 +0200
@@ -987,8 +987,8 @@
apply (simp add: homeomorphic_def homeomorphism_def)
apply (rule_tac x="g \<circ> h" in exI)
apply (rule_tac x="k \<circ> f" in exI)
- apply (auto simp: ghcont kfcont span_superset homeomorphism_apply2 [OF fg] image_comp)
- apply (force simp: o_def homeomorphism_apply2 [OF fg] span_superset)
+ apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp)
+ apply (force simp: o_def homeomorphism_apply2 [OF fg] span_base)
done
finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
show ?thesis