diff -r 1260be3f33a4 -r 400aecdfd71f src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Mon Jul 03 16:46:37 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Jul 04 12:53:01 2023 +0100
@@ -4490,7 +4490,7 @@
   next
     case (Basis s)
     then show ?case
-      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
+      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset_inc)
   qed auto
 next
   fix A