# HG changeset patch
# User blanchet
# Date 1282316655 -7200
# Node ID 5536897d04c24fbf81bc20fb448f62ca0bb3d0dd
# Parent  f7b32911340ba63a5025b2b92aeaea4ef45111cd
remove trivial facts

diff -r f7b32911340b -r 5536897d04c2 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 16:44:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 17:04:15 2010 +0200
@@ -79,10 +79,7 @@
                        |>> AAtom ||> union (op =) ts)
   in do_formula [] end
 
-fun presimplify_term thy =
-  Skip_Proof.make_thm thy
-  #> Meson.presimplify
-  #> prop_of
+val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
 
 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
 fun conceal_bounds Ts t =
@@ -192,7 +189,10 @@
   end
 
 fun make_axiom ctxt presimp (name, th) =
-  (name, make_formula ctxt presimp name Axiom (prop_of th))
+  case make_formula ctxt presimp name Axiom (prop_of th) of
+    FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
+    NONE
+  | formula => SOME (name, formula)
 fun make_conjecture ctxt ts =
   let val last = length ts - 1 in
     map2 (fn j => make_formula ctxt true (Int.toString j)
@@ -236,7 +236,7 @@
                  if exists is_needed ss then map (`Thm.get_name_hint) ths
                  else [])) @
     (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
-    |> map (snd o make_axiom ctxt false)
+    |> map_filter (Option.map snd o make_axiom ctxt false)
   end
 
 fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
@@ -261,7 +261,7 @@
     (* TFrees in the conjecture; TVars in the axioms *)
     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
     val (axiom_names, axioms) =
-      ListPair.unzip (map (make_axiom ctxt true) axioms)
+      ListPair.unzip (map_filter (make_axiom ctxt true) axioms)
     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'