1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Nov 06 21:51:46 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Nov 06 22:18:54 2011 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4  
     1.5  datatype mode = Auto_Try | Try | Normal | Minimize
     1.6  
     1.7 -(* Identifier to distinguish Sledgehammer from other tools using
     1.8 +(* Identifier that distinguishes Sledgehammer from other tools that could use
     1.9     "Async_Manager". *)
    1.10  val das_tool = "Sledgehammer"
    1.11  
    1.12 @@ -147,8 +147,7 @@
    1.13  
    1.14  val select_smt_solver = Context.proof_map o SMT_Config.select_solver
    1.15  
    1.16 -fun is_smt_prover ctxt name =
    1.17 -  member (op =) (SMT_Solver.available_solvers_of ctxt) name
    1.18 +fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
    1.19  
    1.20  fun is_atp_for_format is_format ctxt name =
    1.21    let val thy = Proof_Context.theory_of ctxt in
    1.22 @@ -162,9 +161,9 @@
    1.23  val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
    1.24  val is_ho_atp = is_atp_for_format is_format_higher_order
    1.25  
    1.26 -fun is_prover_supported ctxt name =
    1.27 +fun is_prover_supported ctxt =
    1.28    let val thy = Proof_Context.theory_of ctxt in
    1.29 -    is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name
    1.30 +    is_metis_prover orf is_atp thy orf is_smt_prover ctxt
    1.31    end
    1.32  
    1.33  fun is_prover_installed ctxt =