Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
run blacklist algorithm only if slicing is on
authorblanchet
Tue, 17 May 2011 15:11:36 +0200
changeset 42835 8d723194dedf
parent 42834 40f7691d0539
child 42836 9adf6b3965b3
run blacklist algorithm only if slicing is on
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle