src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 54112 9c0f464d1854
parent 54095 d80743f28fec
child 54124 d3c0cf737b55
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Oct 15 11:49:39 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Oct 15 15:26:58 2013 +0200
     1.3 @@ -439,6 +439,7 @@
     1.4          (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 +    val facts = drop_duplicate_facts thy facts
     1.8      val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
     1.9      val add_pconsts = add_pconsts_in_term thy
    1.10      val chained_ts =