--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 24 23:03:55 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Jun 25 12:41:43 2015 +0200
@@ -181,7 +181,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value mode ctxt =
- [cvc4N, vampireN, z3N, spassN, eN, veritN, e_sineN]
+ [cvc4N, z3N, spassN, eN, vampireN, veritN, e_sineN]
|> map_filter (remotify_prover_if_not_installed ctxt)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))