src/HOL/Tools/ATP_Manager/atp_wrapper.ML

 (*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
     Author:     Fabian Immler, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
 
 Wrapper functions for external ATPs.
 *)
 
 signature ATP_WRAPPER =

   val destdir : string Config.T
   val problem_prefix : string Config.T
   val measure_runtime : bool Config.T
 
   val refresh_systems_on_tptp : unit -> unit
+  val default_atps_param_value : unit -> string
   val setup : theory -> theory
 end;
 
 structure ATP_Wrapper : ATP_WRAPPER =
 struct

 
 val remote_spass =
   tptp_prover (remotify (fst spass))
               (remote_prover_config "SPASS---" "-x" spass_config)
 
+fun maybe_remote (name, _) ({home, ...} : prover_config) =
+  name |> home = "" ? remotify
+
+fun default_atps_param_value () =
+  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
+                     remotify (fst vampire)]
+
 val provers =
   [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
 val prover_setup = fold add_prover provers
 
 val setup =
   destdir_setup
   #> problem_prefix_setup
   #> measure_runtime_setup
-  #> prover_setup;
-
-fun maybe_remote (name, _) ({home, ...} : prover_config) =
-  name |> home = "" ? remotify
-
-val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config,
-                  remotify (fst vampire)] |> space_implode " ")
+  #> prover_setup
+
 end;