# HG changeset patch
# User blanchet
# Date 1305637896 -7200
# Node ID 8d723194dedf5ee369e33e2bb62aa4282f7ba5ee
# Parent  40f7691d05395d7f6d1e22b15bb42ec842ef9da9
run blacklist algorithm only if slicing is on

diff -r 40f7691d0539 -r 8d723194dedf src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 17 15:11:36 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 17 15:11:36 2011 +0200
@@ -610,7 +610,7 @@
                                               atp_proof of
                    [] => result
                  | new_baddies =>
-                   if iter < atp_blacklist_max_iters - 1 then
+                   if slicing andalso iter < atp_blacklist_max_iters - 1 then
                      let val blacklist = new_baddies @ blacklist in
                        result
                        |> maybe_run_slice blacklist (List.last actual_slices)