src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 54142 5f3c1b445253
parent 54112 9c0f464d1854
child 54143 18def1c73c79
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 20:49:19 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 23:41:00 2013 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    val nearly_all_facts :
     1.5      Proof.context -> bool -> fact_override -> unit Symtab.table
     1.6      -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
     1.7 -  val drop_duplicate_facts: theory -> raw_fact list -> raw_fact list
     1.8 +  val drop_duplicate_facts : raw_fact list -> raw_fact list
     1.9  end;
    1.10  
    1.11  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    1.12 @@ -60,7 +60,6 @@
    1.13  
    1.14  (* gracefully handle huge background theories *)
    1.15  val max_facts_for_duplicates = 50000
    1.16 -val max_facts_for_duplicate_matching = 25000
    1.17  val max_facts_for_complex_check = 25000
    1.18  val max_simps_for_clasimpset = 10000
    1.19  
    1.20 @@ -552,11 +551,9 @@
    1.21        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.22      end
    1.23  
    1.24 -fun drop_duplicate_facts thy facts =
    1.25 +fun drop_duplicate_facts facts =
    1.26    let val num_facts = length facts in
    1.27 -    facts |> num_facts <= max_facts_for_duplicates
    1.28 -      ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
    1.29 -          else Pattern.matches thy o swap)
    1.30 +    facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv)
    1.31    end
    1.32  
    1.33  end;