guarded against exception
authorblanchet
Fri Jan 31 13:32:13 2014 +0100 (2014-01-31)
changeset 5520742ad887a1c7c
parent 55206 f7358e55018f
child 55208 11dd3d1da83b
guarded against exception
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:29:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:32:13 2014 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4      end
     1.5  
     1.6  fun remotify_atp_if_not_installed thy name =
     1.7 -  if is_atp_installed thy name then SOME name
     1.8 +  if is_atp thy name andalso is_atp_installed thy name then SOME name
     1.9    else remotify_atp_if_supported_and_not_already_remote thy name
    1.10  
    1.11  fun is_if (@{const_name If}, _) = true