src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 54112 9c0f464d1854
parent 54092 1e2585f56509
child 54142 5f3c1b445253
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 15 11:49:39 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 15 15:26:58 2013 +0200
     1.3 @@ -39,6 +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  end;
     1.9  
    1.10  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    1.11 @@ -545,14 +546,17 @@
    1.12             val facts =
    1.13               all_facts ctxt false ho_atp reserved add chained css
    1.14               |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
    1.15 -            val num_facts = length facts
    1.16           in
    1.17             facts
    1.18 -           |> num_facts <= max_facts_for_duplicates
    1.19 -              ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
    1.20 -                  else Pattern.matches thy o swap)
    1.21           end)
    1.22        |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.23      end
    1.24  
    1.25 +fun drop_duplicate_facts thy 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 +  end
    1.31 +
    1.32  end;