diff --git a/thys/Topological_Groups/Topological_Group.thy b/thys/Topological_Groups/Topological_Group.thy index 3837343efcffc3a51d9d253413f05cf228458a52_dGh5cy9Ub3BvbG9naWNhbF9Hcm91cHMvVG9wb2xvZ2ljYWxfR3JvdXAudGh5..fcd9b94def4d3c7c0d3c1dde56295c7d34974b17_dGh5cy9Ub3BvbG9naWNhbF9Hcm91cHMvVG9wb2xvZ2ljYWxfR3JvdXAudGh5 100644 --- a/thys/Topological_Groups/Topological_Group.thy +++ b/thys/Topological_Groups/Topological_Group.thy @@ -324,7 +324,8 @@ using closure_of_mono by meson moreover have "(conjugation \<sigma>)`(T closure_of N) \<subseteq> T closure_of (conjugation \<sigma>)`N" using h\<sigma> conjugation_homeo - by (meson continuous_map_eq_image_closure_subset homeomorphic_imp_continuous_map) + by (metis continuous_map_image_closure_subset[of T T "conjugation \<sigma>" N] + homeomorphic_imp_continuous_map[of T T "conjugation \<sigma>"]) ultimately show ?thesis by blast qed moreover have "subgroup (T closure_of N) G" using subgroup_closure