src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55453 0b070d098d1a
parent 55452 29ec8680e61f
child 55458 d3b72d260d4a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:17 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:17 2014 +0100
     1.3 @@ -118,17 +118,16 @@
     1.4  
     1.5  val is_atp = member (op =) o supported_atps
     1.6  
     1.7 -fun remotify_atp_if_supported_and_not_already_remote thy name =
     1.8 -  if String.isPrefix remote_prefix name then
     1.9 -    SOME name
    1.10 +fun remotify_atp_if_not_installed thy name =
    1.11 +  if is_atp thy name then
    1.12 +    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then
    1.13 +      SOME name
    1.14 +    else
    1.15 +      let val remote_name = remote_prefix ^ name in
    1.16 +        if is_atp thy remote_name then SOME remote_name else NONE
    1.17 +      end
    1.18    else
    1.19 -    let val remote_name = remote_prefix ^ name in
    1.20 -      if is_atp thy remote_name then SOME remote_name else NONE
    1.21 -    end
    1.22 -
    1.23 -fun remotify_atp_if_not_installed thy name =
    1.24 -  if is_atp thy name andalso is_atp_installed thy name then SOME name
    1.25 -  else remotify_atp_if_supported_and_not_already_remote thy name
    1.26 +    SOME name
    1.27  
    1.28  type params =
    1.29    {debug : bool,