# HG changeset patch
# User wenzelm
# Date 1738703526 -3600
# Node ID 6d3938f1738d0f5245772c728e4c2c651e2cf3e5
# Parent  559eadf415d157af5f9778dc3390968fa59fc6ea
tuned;

diff -r 559eadf415d1 -r 6d3938f1738d src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Feb 04 22:04:12 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Feb 04 22:12:06 2025 +0100
@@ -133,7 +133,7 @@
   | warn_solver _ _ = ()
 
 fun select_solver name context =
-  if not (member (op =) (all_solvers_of' context) name) then
+  if not (defined_solvers context name) then
     error ("Trying to select unknown solver: " ^ quote name)
   else if not (is_available' context name) then
     (warn_solver context name; put_solver name context)