1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:23:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:25:10 2011 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4    let val thy = Proof_Context.theory_of ctxt in
     1.5      case try (get_atp thy) name of
     1.6        SOME {best_slices, ...} =>
     1.7 -      exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
     1.8 +      exists (fn (_, (_, (_, format, _, _))) => is_format format)
     1.9               (best_slices ctxt)
    1.10      | NONE => false
    1.11    end