tuned sledgehammer default provers to only include local ones
authordesharna
Mon, 09 Jan 2023 19:52:32 +0100
changeset 76939 0a46b3dbd5ad
parent 76938 2e849cebd65e
child 76942 c732fa27b60f
tuned sledgehammer default provers to only include local ones
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jan 06 17:59:56 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 09 19:52:32 2023 +0100
@@ -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 =