1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jul 25 12:22:18 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Jul 25 13:15:50 2014 +0200
     1.3 @@ -203,10 +203,9 @@
     1.4    if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
     1.5    else remotify_prover_if_supported_and_not_already_remote ctxt name
     1.6  
     1.7 -(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
     1.8 -   timeout, it makes sense to put E first. *)
     1.9 +(* The first ATP of the list is used by Auto Sledgehammer. *)
    1.10  fun default_provers_param_value mode ctxt =
    1.11 -  [eN, spassN, z3N, e_sineN, vampireN]
    1.12 +  [eN, spassN, z3N, vampireN, e_sineN]
    1.13    |> map_filter (remotify_prover_if_not_installed ctxt)
    1.14    (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
    1.15    |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))