--- 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,