src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 43001 f3492698dfc7
parent 43000 bd424c3dde46
child 43017 944b19ab6003
--- 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 =