--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Dec 15 12:08:41 2010 +0100
@@ -11,12 +11,13 @@
| NONE => default_value
fun extract_relevance_fudge args
- {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
+ {allow_ext, 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} =
- {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
+ {allow_ext = allow_ext,
+ worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
higher_order_irrel_weight =
get args "higher_order_irrel_weight" higher_order_irrel_weight,
abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,