restored old 'remotify' logic -- too many bugs were introduced when refactoring the code

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Feb 14 10:33:57 2014 +0100
@@ -22,6 +22,7 @@
 open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Prover
+open Sledgehammer_Prover_SMT
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MaSh
 open Sledgehammer
@@ -194,11 +195,33 @@
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
+fun is_prover_supported ctxt =
+  let val thy = Proof_Context.theory_of ctxt in
+    is_proof_method orf is_atp thy orf is_smt_prover ctxt
+  end
+
+fun is_prover_installed ctxt =
+  is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+
+fun remotify_prover_if_supported_and_not_already_remote ctxt name =
+  if String.isPrefix remote_prefix name then
+    SOME name
+  else
+    let val remote_name = remote_prefix ^ name in
+      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
+    end
+
+fun remotify_prover_if_not_installed ctxt name =
+  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
+    SOME name
+  else
+    remotify_prover_if_supported_and_not_already_remote ctxt name
+
 (* 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 =
+fun default_provers_param_value mode ctxt =
   [eN, spassN, z3N, e_sineN, vampireN, yicesN]
-  |> map_filter (remotify_atp_if_not_installed thy)
+  |> 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))
   |> implode_param
@@ -209,13 +232,15 @@
   end
 
 fun default_raw_params mode thy =
-  Data.get thy
-  |> fold (AList.default (op =))
-       [("provers", [(case !provers of "" => default_provers_param_value mode thy | s => s)]),
-        ("timeout",
-         let val timeout = Options.default_int @{option sledgehammer_timeout} in
-           [if timeout <= 0 then "none" else string_of_int timeout]
-         end)]
+  let val ctxt = Proof_Context.init_global thy in
+    Data.get thy
+    |> fold (AList.default (op =))
+         [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
+          ("timeout",
+           let val timeout = Options.default_int @{option sledgehammer_timeout} in
+             [if timeout <= 0 then "none" else string_of_int timeout]
+           end)]
+  end
 
 fun extract_params mode default_params override_params =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Feb 14 10:33:57 2014 +0100
@@ -80,7 +80,6 @@
     ((''a * stature) * 'b) list
   val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
     Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
-  val remotify_atp_if_not_installed : theory -> string -> string option
   val isar_supported_prover_of : theory -> string -> string
   val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
     string -> proof_method * play_outcome -> 'a
@@ -118,15 +117,6 @@
 
 val is_atp = member (op =) o supported_atps
 
-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 NONE
-  else
-    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,
    verbose : bool,
@@ -260,7 +250,8 @@
 
 fun isar_supported_prover_of thy name =
   if is_atp thy name then name
-  else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
+  else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
+  else name
 
 (* FIXME: See the analogous logic in the function "maybe_minimize" in
    "sledgehammer_prover_minimize.ML". *)