# HG changeset patch
# User desharna
# Date 1741360568 -3600
# Node ID f3db31c8acbcc9c3fc3cfc7786a66a81073037d0
# Parent  3505a7b02fc26fd5abfc0497e8de5893029785b6
disabled tactic_provers in Sledgehammer

diff -r 3505a7b02fc2 -r f3db31c8acbc src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Mar 06 08:16:46 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Mar 07 16:16:08 2025 +0100
@@ -171,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) (smt_solvers ctxt @ local_atps @ tactic_provers)
+  filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps)
   |> implode_param
 
 fun set_default_raw_param param thy =