# HG changeset patch
# User blanchet
# Date 1391171533 -3600
# Node ID 42ad887a1c7cc4b73a4eae7f801ddf9c906c3254
# Parent  f7358e55018faeb0566eec47e22d7de231e58bc6
guarded against exception

diff -r f7358e55018f -r 42ad887a1c7c src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:29:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:32:13 2014 +0100
@@ -158,7 +158,7 @@
     end
 
 fun remotify_atp_if_not_installed thy name =
-  if is_atp_installed thy name then SOME name
+  if is_atp thy name andalso is_atp_installed thy name then SOME name
   else remotify_atp_if_supported_and_not_already_remote thy name
 
 fun is_if (@{const_name If}, _) = true