# HG changeset patch
# User paulson
# Date 1673348780 0
# Node ID c732fa27b60f6cd4eb412e70d1d2babbdcdbadc3
# Parent  0a46b3dbd5ad18212c37c144587af2f0922bf8ca# Parent  5e033f907bcc0948a4d5d623e1b56d67f21747e8
merged

diff -r 5e033f907bcc -r c732fa27b60f src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 09 17:16:22 2023 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Jan 10 11:06:20 2023 +0000
@@ -163,7 +163,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 @ non_dummy_atps)
+  filter (is_prover_installed ctxt) (smts ctxt @ local_atps)
   |> implode_param
 
 fun set_default_raw_param param thy =