src/HOL/Tools/ATP_Manager/atp_wrapper.ML
changeset 36371 8c83ea1a7740
parent 36370 a4f601daa175
child 36376 e83d52a52449
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 15:48:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 23 16:15:35 2010 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
     1.5      Author:     Fabian Immler, TU Muenchen
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7  
     1.8  Wrapper functions for external ATPs.
     1.9  *)
    1.10 @@ -14,6 +15,7 @@
    1.11    val measure_runtime : bool Config.T
    1.12  
    1.13    val refresh_systems_on_tptp : unit -> unit
    1.14 +  val default_atps_param_value : unit -> string
    1.15    val setup : theory -> theory
    1.16  end;
    1.17  
    1.18 @@ -389,6 +391,13 @@
    1.19    tptp_prover (remotify (fst spass))
    1.20                (remote_prover_config "SPASS---" "-x" spass_config)
    1.21  
    1.22 +fun maybe_remote (name, _) ({home, ...} : prover_config) =
    1.23 +  name |> home = "" ? remotify
    1.24 +
    1.25 +fun default_atps_param_value () =
    1.26 +  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
    1.27 +                     remotify (fst vampire)]
    1.28 +
    1.29  val provers =
    1.30    [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
    1.31  val prover_setup = fold add_prover provers
    1.32 @@ -397,11 +406,6 @@
    1.33    destdir_setup
    1.34    #> problem_prefix_setup
    1.35    #> measure_runtime_setup
    1.36 -  #> prover_setup;
    1.37 +  #> prover_setup
    1.38  
    1.39 -fun maybe_remote (name, _) ({home, ...} : prover_config) =
    1.40 -  name |> home = "" ? remotify
    1.41 -
    1.42 -val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config,
    1.43 -                  remotify (fst vampire)] |> space_implode " ")
    1.44  end;