# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1755177920 -3600
# Node ID 987cd5e21f722112e28ca29838ffcff15df7b9ea
# Parent  a2a860cd32152484e5ac35e15cef467d1c56d077
Removed an SMT call

diff -r a2a860cd3215 -r 987cd5e21f72 src/HOL/Analysis/Urysohn.thy
--- a/src/HOL/Analysis/Urysohn.thy	Wed Aug 13 19:40:09 2025 +0200
+++ b/src/HOL/Analysis/Urysohn.thy	Thu Aug 14 14:25:20 2025 +0100
@@ -361,8 +361,8 @@
       using that
       by (simp add: contf good_def continuous_map_diff continuous_map_from_subtopology)
     then have "closedin (subtopology X S) SA"
-      unfolding SA_def
-      by (smt (verit, del_insts) closed_closedin continuous_map_closedin Collect_cong S_eq closed_real_atMost)
+      unfolding SA_def continuous_map_closedin
+      by (metis (full_types) S_eq closed_atMost closed_closedin)
     then have "closedin X SA"
       using \<open>closedin X S\<close> closedin_trans_full by blast
     moreover have  "closedin (subtopology X S) SB"