--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 31 10:13:04 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 31 13:12:56 2010 +0200
@@ -6,7 +6,8 @@
struct
val relevance_filter_args =
- [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
+ [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
+ ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),