# HG changeset patch
# User blanchet
# Date 1314714310 -7200
# Node ID d34ff13371e025b2bcb06a481b781e0fffe2076f
# Parent  b054ca3f07b57bdc6c665fcee87ffde1e830a3d0
fixed just introduced silly bug

diff -r b054ca3f07b5 -r d34ff13371e0 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:23:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:25:10 2011 +0200
@@ -156,7 +156,7 @@
   let val thy = Proof_Context.theory_of ctxt in
     case try (get_atp thy) name of
       SOME {best_slices, ...} =>
-      exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
+      exists (fn (_, (_, (_, format, _, _))) => is_format format)
              (best_slices ctxt)
     | NONE => false
   end