# HG changeset patch
# User blanchet
# Date 1392304903 -3600
# Node ID d3b72d260d4a1317b42eb1ba1433f68b40f3362b
# Parent  e373c9f60db1055830befa3c138d4d1d67537f5f
do the right thing with provers that exist only remotely (e.g. e_sine)

diff -r e373c9f60db1 -r d3b72d260d4a src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Feb 13 15:51:54 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Feb 13 16:21:43 2014 +0100
@@ -197,7 +197,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put E first. *)
 fun default_provers_param_value mode thy =
-  [eN, spassN, z3N, vampireN, e_sineN, yicesN]
+  [eN, spassN, z3N, e_sineN, vampireN, yicesN]
   |> map_filter (remotify_atp_if_not_installed thy)
   (* 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))
diff -r e373c9f60db1 -r d3b72d260d4a src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 15:51:54 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 16:21:43 2014 +0100
@@ -120,14 +120,12 @@
 
 fun remotify_atp_if_not_installed thy name =
   if is_atp thy name then
-    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then
-      SOME name
-    else
-      let val remote_name = remote_prefix ^ name in
-        if is_atp thy remote_name then SOME remote_name else NONE
-      end
+    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then SOME name
+    else NONE
   else
-    SOME name
+    let val remote_name = remote_prefix ^ name in
+      SOME (if is_atp thy remote_name then remote_name else name)
+    end
 
 type params =
   {debug : bool,