1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 09:33:01 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 09 09:33:50 2011 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4    val vampireN : string
     1.5    val leo2N : string
     1.6    val satallaxN : string
     1.7 -  val sine_eN : string
     1.8 +  val e_sineN : string
     1.9    val snarkN : string
    1.10 -  val tofof_eN : string
    1.11 +  val e_tofofN : string
    1.12    val waldmeisterN : string
    1.13    val z3_atpN : string
    1.14    val remote_prefix : string
    1.15 @@ -108,9 +108,9 @@
    1.16  val z3_atpN = "z3_atp"
    1.17  val leo2N = "leo2"
    1.18  val satallaxN = "satallax"
    1.19 -val sine_eN = "sine_e"
    1.20 +val e_sineN = "e_sine"
    1.21  val snarkN = "snark"
    1.22 -val tofof_eN = "tofof_e"
    1.23 +val e_tofofN = "e_tofof"
    1.24  val waldmeisterN = "waldmeister"
    1.25  val remote_prefix = "remote_"
    1.26  
    1.27 @@ -422,15 +422,15 @@
    1.28  val remote_satallax =
    1.29    remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
    1.30               (K (64, "simple_higher") (* FUDGE *))
    1.31 -val remote_sine_e =
    1.32 -  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
    1.33 +val remote_e_sine =
    1.34 +  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
    1.35               Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
    1.36  val remote_snark =
    1.37    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
    1.38               [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
    1.39               [TFF, FOF] (K (100, "simple") (* FUDGE *))
    1.40 -val remote_tofof_e =
    1.41 -  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
    1.42 +val remote_e_tofof =
    1.43 +  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
    1.44               Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
    1.45  val remote_waldmeister =
    1.46    remote_atp waldmeisterN "Waldmeister" ["710"]
    1.47 @@ -462,7 +462,7 @@
    1.48  
    1.49  val atps =
    1.50    [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
    1.51 -   remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
    1.52 +   remote_leo2, remote_satallax, remote_e_sine, remote_snark, remote_e_tofof,
    1.53     remote_waldmeister]
    1.54  val setup = fold add_atp atps
    1.55  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 09 09:33:01 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 09 09:33:50 2011 +0200
     2.3 @@ -199,7 +199,7 @@
     2.4  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
     2.5     timeout, it makes sense to put SPASS first. *)
     2.6  fun default_provers_param_value ctxt =
     2.7 -  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
     2.8 +  [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
     2.9    |> map_filter (remotify_prover_if_not_installed ctxt)
    2.10    |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
    2.11                                    max_default_remote_threads)