fixed just introduced silly bug
authorblanchet
Tue, 30 Aug 2011 16:25:10 +0200
changeset 44599 d34ff13371e0
parent 44598 b054ca3f07b5
child 44600 426834f253c8
fixed just introduced silly bug
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