# HG changeset patch
# User blanchet
# Date 1382047531 -7200
# Node ID 18def1c73c79a4a2fb58dac146b1e5852e3d4343
# Parent  5f3c1b445253b33cf42cfc70709c2fb275552adf
make sure add: doesn't add duplicates, and works for [no_atp] facts

diff -r 5f3c1b445253 -r 18def1c73c79 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Oct 17 23:41:00 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Oct 18 00:05:31 2013 +0200
@@ -128,6 +128,7 @@
                Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
                hyp_ts concl_t
            |> filter (is_appropriate_prop o prop_of o snd)
+           |> Sledgehammer_Fact.drop_duplicate_facts
            |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
                   (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t
             |> map (fst o fst)
diff -r 5f3c1b445253 -r 18def1c73c79 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Oct 17 23:41:00 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Oct 18 00:05:31 2013 +0200
@@ -245,6 +245,7 @@
               val suggs =
                 old_facts
                 |> linearize ? filter_accessible_from th
+                |> Sledgehammer_Fact.drop_duplicate_facts
                 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t
                 |> map (nickname_of_thm o snd)
             in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end
diff -r 5f3c1b445253 -r 18def1c73c79 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 23:41:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Oct 18 00:05:31 2013 +0200
@@ -544,7 +544,8 @@
            val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
            val facts =
              all_facts ctxt false ho_atp reserved add chained css
-             |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
+             |> filter_out ((member Thm.eq_thm_prop del orf
+               (No_ATPs.member ctxt andf not o member Thm.eq_thm_prop add)) o snd)
          in
            facts
          end)
diff -r 5f3c1b445253 -r 18def1c73c79 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 23:41:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 18 00:05:31 2013 +0200
@@ -1317,16 +1317,19 @@
              if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
           else
             (false, mepoN)
+
+      val unique_facts = drop_duplicate_facts facts
       val add_ths = Attrib.eval_thms ctxt add
+
       fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
       fun add_and_take accepts =
         (case add_ths of
            [] => accepts
-         | _ => (facts |> filter in_add |> map fact_of_raw_fact) @
+         | _ => (unique_facts |> filter in_add |> map fact_of_raw_fact) @
                 (accepts |> filter_out in_add))
         |> take max_facts
       fun mepo () =
-        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t facts
+        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
          |> weight_facts_steeply, [])
       fun mash () =
         mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts
diff -r 5f3c1b445253 -r 18def1c73c79 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 23:41:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Oct 18 00:05:31 2013 +0200
@@ -439,7 +439,6 @@
         (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
   let
     val thy = Proof_Context.theory_of ctxt
-    val facts = drop_duplicate_facts facts
     val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
     val add_pconsts = add_pconsts_in_term thy
     val chained_ts =