--- 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
@@ -11,14 +11,13 @@
| NONE => default_value
fun extract_relevance_fudge args
- {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,
+ {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,
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 =
+ local_bonus, assum_bonus, chained_bonus, max_imperfect, max_imperfect_exp,
+ threshold_divisor, ridiculous_threshold} =
+ {local_const_multiplier =
get args "local_const_multiplier" local_const_multiplier,
worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
higher_order_irrel_weight =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu May 12 15:29:19 2011 +0200
@@ -10,8 +10,7 @@
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
type relevance_fudge =
- {allow_ext : bool,
- local_const_multiplier : real,
+ {local_const_multiplier : real,
worse_irrel_freq : real,
higher_order_irrel_weight : real,
abs_rel_weight : real,
@@ -83,8 +82,7 @@
| is_locality_global _ = true
type relevance_fudge =
- {allow_ext : bool,
- local_const_multiplier : real,
+ {local_const_multiplier : real,
worse_irrel_freq : real,
higher_order_irrel_weight : real,
abs_rel_weight : real,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:19 2011 +0200
@@ -163,8 +163,7 @@
(* FUDGE *)
val atp_relevance_fudge =
- {allow_ext = true,
- local_const_multiplier = 1.5,
+ {local_const_multiplier = 1.5,
worse_irrel_freq = 100.0,
higher_order_irrel_weight = 1.05,
abs_rel_weight = 0.5,
@@ -186,8 +185,7 @@
(* FUDGE (FIXME) *)
val smt_relevance_fudge =
- {allow_ext = false,
- local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
+ {local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
abs_rel_weight = #abs_rel_weight atp_relevance_fudge,