# HG changeset patch
# User blanchet
# Date 1284193372 -7200
# Node ID da4e98cb20053eaa8bf2fb0cd539431ebac0a421
# Parent  ad9a1f9b05585d1e3e05c1643b7d21789a59ce56
change order of default ATPs;
put SPASS first so that it's picked up by Auto Sledgehammer

diff -r ad9a1f9b0558 -r da4e98cb2005 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Sep 11 10:21:52 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Sep 11 10:22:52 2010 +0200
@@ -303,9 +303,11 @@
 fun maybe_remote (name, config) =
   name |> not (is_installed config) ? remotify_name
 
+(* The first prover of the list is used by Auto Sledgehammer. Because of the low
+   timeout, it makes sense to put SPASS first. *)
 fun default_atps_param_value () =
-  space_implode " " ([maybe_remote e] @
-                     (if is_installed (snd spass) then [fst spass] else []) @
+  space_implode " " ((if is_installed (snd spass) then [fst spass] else []) @
+                     [maybe_remote e] @
                      [if forall (is_installed o snd) [e, spass] then
                         remotify_name (fst vampire)
                       else