--- a/src/HOL/Analysis/Function_Topology.thy Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy Tue Mar 31 15:51:15 2020 +0200
@@ -198,7 +198,7 @@
have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
using openin_topspace not_finite_existsD by auto
then show "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<subseteq> topspace (product_topology T I)"
- unfolding product_topology_def using PiE_def by (auto simp add: topology_generated_by_topspace)
+ unfolding product_topology_def using PiE_def by (auto)
qed
lemma product_topology_basis: