--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 27 10:30:07 2011 +0200
@@ -495,8 +495,8 @@
((name, loc), t) =
case (keep_trivial,
make_formula ctxt format type_sys eq_as_iff presimp name loc Axiom t) of
- (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
- NONE
+ (false, formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
+ if s = tptp_true then NONE else SOME formula
| (_, formula) => SOME formula
fun make_conjecture ctxt format prem_kind type_sys ts =