# HG changeset patch
# User blanchet
# Date 1428512152 -7200
# Node ID b622365f181cfc7d1320a2809b836cd97533c9f8
# Parent  a965060dcbb8a9f48a28fe73ebb7b017f986f01e
reorder provers to reflect current eval results

diff -r a965060dcbb8 -r b622365f181c src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 08 18:48:56 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 08 18:55:52 2015 +0200
@@ -181,7 +181,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [spassN, cvc4N, vampireN, eN, z3N, veritN, e_sineN]
+  [cvc4N, vampireN, z3N, spassN, eN, 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))