# HG changeset patch
# User blanchet
# Date 1314713502 -7200
# Node ID 03bbadb252db12d7ee12b9c80e42bf443813f56d
# Parent  2621046c550a1808abf04b2d0268d1031a36a2c3
tuning

diff -r 2621046c550a -r 03bbadb252db src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:07:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:11:42 2011 +0200
@@ -152,20 +152,7 @@
 fun is_smt_prover ctxt name =
   member (op =) (SMT_Solver.available_solvers_of ctxt) name
 
-fun is_ho_atp ctxt name =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in case try (get_atp thy) name of
-      SOME {best_slices, ...} =>
-        exists (fn cfg => case cfg of
-                   (_, (_, (_, THF _, _, _))) => true
-                 | _ => false
-               )
-               (best_slices ctxt)
-    | NONE => false
-  end
-
-fun is_unit_equational_atp ctxt name =
+fun is_atp_for_format is_format ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     case try (get_atp thy) name of
       SOME {best_slices, ...} =>
@@ -174,6 +161,9 @@
     | NONE => false
   end
 
+val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
+val is_ho_atp = is_atp_for_format is_format_thf
+
 fun is_prover_supported ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name