src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55475 b8ebbcc5e49a
parent 55458 d3b72d260d4a
child 56081 72fad75baf7e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Feb 14 10:33:57 2014 +0100
     1.3 @@ -80,7 +80,6 @@
     1.4      ((''a * stature) * 'b) list
     1.5    val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
     1.6      Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
     1.7 -  val remotify_atp_if_not_installed : theory -> string -> string option
     1.8    val isar_supported_prover_of : theory -> string -> string
     1.9    val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
    1.10      string -> proof_method * play_outcome -> 'a
    1.11 @@ -118,15 +117,6 @@
    1.12  
    1.13  val is_atp = member (op =) o supported_atps
    1.14  
    1.15 -fun remotify_atp_if_not_installed thy name =
    1.16 -  if is_atp thy name then
    1.17 -    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then SOME name
    1.18 -    else NONE
    1.19 -  else
    1.20 -    let val remote_name = remote_prefix ^ name in
    1.21 -      SOME (if is_atp thy remote_name then remote_name else name)
    1.22 -    end
    1.23 -
    1.24  type params =
    1.25    {debug : bool,
    1.26     verbose : bool,
    1.27 @@ -260,7 +250,8 @@
    1.28  
    1.29  fun isar_supported_prover_of thy name =
    1.30    if is_atp thy name then name
    1.31 -  else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
    1.32 +  else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
    1.33 +  else name
    1.34  
    1.35  (* FIXME: See the analogous logic in the function "maybe_minimize" in
    1.36     "sledgehammer_prover_minimize.ML". *)