# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID f3492698dfc752e82d799f370cbb149d20a7b6c4
# Parent  bd424c3dde464a88929e90faa46e401616341e2e
fixed trivial fact detection

diff -r bd424c3dde46 -r f3492698dfc7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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 =