improved whitelist (cf. be1874de8344)

--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 04 18:14:58 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 04 18:14:58 2014 +0200
@@ -848,8 +848,7 @@
               if size s > max_readable_name_size then
                 String.substring (s, 0, max_readable_name_size div 2 - 4) ^
                 string_of_int (hash_string (cleanup_mirabelle_name full_name)) ^
-                String.extract (s, size s - max_readable_name_size div 2 + 4,
-                                NONE)
+                String.extract (s, size s - max_readable_name_size div 2 + 4, NONE)
               else
                 s)
        |> (fn s =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun May 04 18:14:58 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun May 04 18:14:58 2014 +0200
@@ -123,7 +123,7 @@
    ("no_smt_proofs", "smt_proofs")]
 
 val params_not_for_minimize =
-  ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
+  ["provers", "blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
 
 val property_dependent_params = ["provers", "timeout"]