# 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 =