# HG changeset patch
# User blanchet
# Date 1282572761 -7200
# Node ID 1bf1e21d313694e8f5313da6c91ff76ec11760eb
# Parent  0b1a63d0680586a6156129cce338e0dfbde6b9a3
prevent double inclusion of the fact "True_or_False" in TPTP problems

diff -r 0b1a63d06805 -r 1bf1e21d3136 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 15:30:42 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 16:12:41 2010 +0200
@@ -208,7 +208,7 @@
    default_max_relevant_per_iter = 45 (* FUDGE *),
    default_theory_relevant = false,
    explicit_forall = false,
-   use_conjecture_for_hypotheses = true}
+   use_conjecture_for_hypotheses = false} (*###*)
 
 val vampire = ("vampire", vampire_config)
 
diff -r 0b1a63d06805 -r 1bf1e21d3136 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 15:30:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 16:12:41 2010 +0200
@@ -223,13 +223,13 @@
    (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
    (["c_COMBS"], @{thms COMBS_def})]
 val optional_typed_helpers =
-  [(["c_True", "c_False"], @{thms True_or_False}),
-   (["c_If"], @{thms if_True if_False True_or_False})]
+  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
+   (["c_If"], @{thms if_True if_False})]
 val mandatory_helpers = @{thms fequal_def}
 
 val init_counters =
-  Symtab.make (maps (maps (map (rpair 0) o fst))
-                    [optional_helpers, optional_typed_helpers])
+  [optional_helpers, optional_typed_helpers] |> maps (maps fst) 
+  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
 
 fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   let
@@ -472,7 +472,7 @@
         (is_tptp_variable s andalso not (member (op =) bounds name))
           ? insert (op =) name
         #> fold (term_vars bounds) tms
-    fun formula_vars bounds (AQuant (q, xs, phi)) =
+    fun formula_vars bounds (AQuant (_, xs, phi)) =
         formula_vars (xs @ bounds) phi
       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
       | formula_vars bounds (AAtom tm) = term_vars bounds tm