--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Oct 17 23:41:00 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 18 00:05:31 2013 +0200
@@ -128,6 +128,7 @@
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
+ |> Sledgehammer_Fact.drop_duplicate_facts
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params
(the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t
|> map (fst o fst)