--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
@@ -14,9 +14,9 @@
{allow_ext, local_const_multiplier, worse_irrel_freq,
higher_order_irrel_weight, abs_rel_weight, abs_irrel_weight,
skolem_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight,
- intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus,
- chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor,
- ridiculous_threshold} =
+ chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
+ local_bonus, assum_bonus, chained_bonus, max_imperfect,
+ max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
{allow_ext = allow_ext,
local_const_multiplier =
get args "local_const_multiplier" local_const_multiplier,
@@ -30,6 +30,8 @@
get args "theory_const_rel_weight" theory_const_rel_weight,
theory_const_irrel_weight =
get args "theory_const_irrel_weight" theory_const_irrel_weight,
+ chained_const_irrel_weight =
+ get args "chained_const_irrel_weight" chained_const_irrel_weight,
intro_bonus = get args "intro_bonus" intro_bonus,
elim_bonus = get args "elim_bonus" elim_bonus,
simp_bonus = get args "simp_bonus" simp_bonus,