# HG changeset patch
# User blanchet
# Date 1381843618 -7200
# Node ID 9c0f464d1854d1394e42d7c1818f158ef38acbf3
# Parent  fb6ef69b8c8528cf21fe2051f7f42f54eb2ddff0
drop only real duplicates, not subsumed facts -- this confuses MaSh

diff -r fb6ef69b8c85 -r 9c0f464d1854 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 15 11:49:39 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 15 15:26:58 2013 +0200
@@ -39,6 +39,7 @@
   val nearly_all_facts :
     Proof.context -> bool -> fact_override -> unit Symtab.table
     -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
+  val drop_duplicate_facts: theory -> raw_fact list -> raw_fact list
 end;
 
 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -545,14 +546,17 @@
            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)
-            val num_facts = length facts
          in
            facts
-           |> num_facts <= max_facts_for_duplicates
-              ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
-                  else Pattern.matches thy o swap)
          end)
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
     end
 
+fun drop_duplicate_facts thy facts =
+  let val num_facts = length facts in
+    facts |> num_facts <= max_facts_for_duplicates
+      ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
+          else Pattern.matches thy o swap)
+  end
+
 end;
diff -r fb6ef69b8c85 -r 9c0f464d1854 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Oct 15 11:49:39 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Oct 15 15:26:58 2013 +0200
@@ -439,6 +439,7 @@
         (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
   let
     val thy = Proof_Context.theory_of ctxt
+    val facts = drop_duplicate_facts thy facts
     val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
     val add_pconsts = add_pconsts_in_term thy
     val chained_ts =