--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Feb 25 17:37:41 2025 +0100
@@ -25,6 +25,7 @@
open Sledgehammer_ATP_Systems
open Sledgehammer_Prover
open Sledgehammer_Prover_SMT
+open Sledgehammer_Prover_Tactic
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
open Sledgehammer
@@ -170,7 +171,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value ctxt =
\<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
- filter (is_prover_installed ctxt) (smts ctxt @ local_atps)
+ filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps @ tactic_provers)
|> implode_param
fun set_default_raw_param param thy =