Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
guarded against exception
authorblanchet
Fri, 31 Jan 2014 13:32:13 +0100
changeset 55207 42ad887a1c7c
parent 55206 f7358e55018f
child 55208 11dd3d1da83b
guarded against exception
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle