# HG changeset patch
# User blanchet
# Date 1283184427 -7200
# Node ID a8aeaf9d4ca5ec74d5f2f645db9d84ca190ce37a
# Parent  5e760c0f81a6e813f9c8b9c6a62e61b606ebf91b
adjust Mirabelle

diff -r 5e760c0f81a6 -r a8aeaf9d4ca5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 17:14:54 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 18:07:07 2010 +0200
@@ -12,10 +12,10 @@
    ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus),
    ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
    ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
+   ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
+   ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp),
    ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
-   ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold),
-   ("max_max_imperfect_fudge_factor",
-    Sledgehammer_Fact_Filter.max_max_imperfect_fudge_factor)]
+   ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)]
 
 structure Prooftab =
   Table(type key = int * int val ord = prod_ord int_ord int_ord);