1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -14,9 +14,9 @@
     1.4        {allow_ext, local_const_multiplier, worse_irrel_freq,
     1.5         higher_order_irrel_weight, abs_rel_weight, abs_irrel_weight,
     1.6         skolem_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight,
     1.7 -       intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus,
     1.8 -       chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor,
     1.9 -       ridiculous_threshold} =
    1.10 +       chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
    1.11 +       local_bonus, assum_bonus, chained_bonus, max_imperfect,
    1.12 +       max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
    1.13    {allow_ext = allow_ext,
    1.14     local_const_multiplier =
    1.15         get args "local_const_multiplier" local_const_multiplier,
    1.16 @@ -30,6 +30,8 @@
    1.17         get args "theory_const_rel_weight" theory_const_rel_weight,
    1.18     theory_const_irrel_weight =
    1.19         get args "theory_const_irrel_weight" theory_const_irrel_weight,
    1.20 +   chained_const_irrel_weight =
    1.21 +       get args "chained_const_irrel_weight" chained_const_irrel_weight,
    1.22     intro_bonus = get args "intro_bonus" intro_bonus,
    1.23     elim_bonus = get args "elim_bonus" elim_bonus,
    1.24     simp_bonus = get args "simp_bonus" simp_bonus,