# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 2a9dcff63b8098ced156f78d7b406557a35df968
# Parent  7e4ac591d983e5daf228dc795dc0d6d211750089
remove unused parameter

diff -r 7e4ac591d983 -r 2a9dcff63b80 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- 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 =
diff -r 7e4ac591d983 -r 2a9dcff63b80 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- 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,
diff -r 7e4ac591d983 -r 2a9dcff63b80 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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,