# HG changeset patch
# User desharna
# Date 1653652000 -7200
# Node ID d9b23902692dd811871ba4c75190eb6627b0a55c
# Parent  84e6f9b542e2a2d8b3466fae8768438ffb7fcfad
excluded dummy ATPs from Sledgehammer's default provers

diff -r 84e6f9b542e2 -r d9b23902692d src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri May 27 13:46:40 2022 +0200
@@ -41,7 +41,9 @@
   val refresh_systems_on_tptp : unit -> unit
   val local_atps : string list
   val remote_atps : string list
-  val atps : string list
+  val dummy_atps : string list
+  val non_dummy_atps : string list
+  val all_atps : string list
 end;
 
 structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS =
@@ -568,13 +570,18 @@
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, zipperposition]
 val remote_atps =
   [remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
-val atps = local_atps @ remote_atps
+   remote_waldmeister, remote_zipperposition]
+val dummy_atps =
+  [dummy_fof, dummy_tfx, dummy_thf, dummy_thf_reduced]
+val non_dummy_atps = local_atps @ remote_atps
+val all_atps = non_dummy_atps @ dummy_atps
 
-val _ = Theory.setup (fold add_atp atps)
+val _ = Theory.setup (fold add_atp all_atps)
 
 val local_atps = map fst local_atps
 val remote_atps = map fst remote_atps
-val atps = map fst atps
+val dummy_atps = map fst dummy_atps
+val non_dummy_atps = map fst non_dummy_atps
+val all_atps = map fst all_atps
 
 end;
diff -r 84e6f9b542e2 -r d9b23902692d src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 27 13:46:40 2022 +0200
@@ -162,7 +162,8 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value ctxt =
-  filter (is_prover_installed ctxt) (smts ctxt @ atps) \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+  \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+  filter (is_prover_installed ctxt) (smts ctxt @ non_dummy_atps)
   |> implode_param
 
 fun set_default_raw_param param thy =
diff -r 84e6f9b542e2 -r d9b23902692d src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 27 13:46:40 2022 +0200
@@ -127,7 +127,7 @@
   | induction_rules_of_string "instantiate" = SOME Instantiate
   | induction_rules_of_string _ = NONE
 
-val is_atp = member (op =) atps
+val is_atp = member (op =) all_atps
 
 type params =
   {debug : bool,