# HG changeset patch
# User blanchet
# Date 1382046060 -7200
# Node ID 5f3c1b445253b33cf42cfc70709c2fb275552adf
# Parent  f57f8e7a879f54a93bc9c280618ef6313ef0d9e0
no fact subsumption -- this only confuses later code, e.g. 'add:'

diff -r f57f8e7a879f -r 5f3c1b445253 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 20:49:19 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 23:41:00 2013 +0200
@@ -39,7 +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
+  val drop_duplicate_facts : raw_fact list -> raw_fact list
 end;
 
 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -60,7 +60,6 @@
 
 (* gracefully handle huge background theories *)
 val max_facts_for_duplicates = 50000
-val max_facts_for_duplicate_matching = 25000
 val max_facts_for_complex_check = 25000
 val max_simps_for_clasimpset = 10000
 
@@ -552,11 +551,9 @@
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
     end
 
-fun drop_duplicate_facts thy facts =
+fun drop_duplicate_facts 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)
+    facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv)
   end
 
 end;
diff -r f57f8e7a879f -r 5f3c1b445253 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 20:49:19 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 23:41:00 2013 +0200
@@ -439,7 +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 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 =