src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
changeset 38941 e2c95e3263a4
parent 38938 2b93dbc07778
child 38988 483879af0643
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 20:20:10 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 20:23:32 2010 +0200
@@ -7,6 +7,8 @@
 
 val relevance_filter_args =
   [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
+   ("higher_order_irrel_weight",
+    Sledgehammer_Fact_Filter.higher_order_irrel_weight),
    ("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),