# HG changeset patch
# User blanchet
# Date 1379709570 -7200
# Node ID be1874de8344b335c0db6dfb579eba76dc5b3257
# Parent  8d1a059ebcdbeccd02d15e503948ab4b81a89eef
tuning (use a blacklist instead of a whitelist)

diff -r 8d1a059ebcdb -r be1874de8344 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 20 22:39:30 2013 +0200
@@ -123,12 +123,9 @@
    ("dont_minimize_isar", "isar_minimize"),
    ("no_preplay_trace", "preplay_trace")] (* TODO: document *)
 
-val params_for_minimize =
-  ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
-   "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
-   "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
-(* TODO: add isar_compress_degree, merge_timeout_slack,  preplay_trace,
-   isar_try0, isar_minimize? *)
+val params_not_for_minimize =
+  ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice",
+   "minimize"];
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -345,7 +342,7 @@
 val default_minimize_prover = metisN
 
 fun is_raw_param_relevant_for_minimize (name, _) =
-  member (op =) params_for_minimize name
+  not (member (op =) params_not_for_minimize name)
 fun string_of_raw_param (key, values) =
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 fun nice_string_of_raw_param (p as (key, ["false"])) =