# HG changeset patch
# User blanchet
# Date 1399220098 -7200
# Node ID 3e369d8610c415560d01c321f563e3ac7ba12046
# Parent  9df717fef2bbb85612732ef952f6735e0baf55e1
improved whitelist (cf. be1874de8344)

diff -r 9df717fef2bb -r 3e369d8610c4 src/HOL/Tools/ATP/atp_problem.ML
--- 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 =>
diff -r 9df717fef2bb -r 3e369d8610c4 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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"]