remove unused parameter
authorblanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 427382a9dcff63b80
parent 42737 7e4ac591d983
child 42739 017e5dac8642
remove unused parameter
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     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 @@ -11,14 +11,13 @@
     1.4    | NONE => default_value
     1.5  
     1.6  fun extract_relevance_fudge args
     1.7 -      {allow_ext, local_const_multiplier, worse_irrel_freq,
     1.8 -       higher_order_irrel_weight, abs_rel_weight, abs_irrel_weight,
     1.9 -       skolem_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight,
    1.10 +      {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight,
    1.11 +       abs_rel_weight, abs_irrel_weight, skolem_irrel_weight,
    1.12 +       theory_const_rel_weight, theory_const_irrel_weight,
    1.13         chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
    1.14 -       local_bonus, assum_bonus, chained_bonus, max_imperfect,
    1.15 -       max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
    1.16 -  {allow_ext = allow_ext,
    1.17 -   local_const_multiplier =
    1.18 +       local_bonus, assum_bonus, chained_bonus, max_imperfect, max_imperfect_exp,
    1.19 +       threshold_divisor, ridiculous_threshold} =
    1.20 +  {local_const_multiplier =
    1.21         get args "local_const_multiplier" local_const_multiplier,
    1.22     worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
    1.23     higher_order_irrel_weight =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -10,8 +10,7 @@
     2.4    datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
     2.5  
     2.6    type relevance_fudge =
     2.7 -    {allow_ext : bool,
     2.8 -     local_const_multiplier : real,
     2.9 +    {local_const_multiplier : real,
    2.10       worse_irrel_freq : real,
    2.11       higher_order_irrel_weight : real,
    2.12       abs_rel_weight : real,
    2.13 @@ -83,8 +82,7 @@
    2.14    | is_locality_global _ = true
    2.15  
    2.16  type relevance_fudge =
    2.17 -  {allow_ext : bool,
    2.18 -   local_const_multiplier : real,
    2.19 +  {local_const_multiplier : real,
    2.20     worse_irrel_freq : real,
    2.21     higher_order_irrel_weight : real,
    2.22     abs_rel_weight : real,
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
     3.3 @@ -163,8 +163,7 @@
     3.4  
     3.5  (* FUDGE *)
     3.6  val atp_relevance_fudge =
     3.7 -  {allow_ext = true,
     3.8 -   local_const_multiplier = 1.5,
     3.9 +  {local_const_multiplier = 1.5,
    3.10     worse_irrel_freq = 100.0,
    3.11     higher_order_irrel_weight = 1.05,
    3.12     abs_rel_weight = 0.5,
    3.13 @@ -186,8 +185,7 @@
    3.14  
    3.15  (* FUDGE (FIXME) *)
    3.16  val smt_relevance_fudge =
    3.17 -  {allow_ext = false,
    3.18 -   local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
    3.19 +  {local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
    3.20     worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
    3.21     higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
    3.22     abs_rel_weight = #abs_rel_weight atp_relevance_fudge,