# HG changeset patch
# User blanchet
# Date 1305274243 -7200
# Node ID 69640564a3941ff667c0c6fe0d7c52c943da0802
# Parent  87389311ba78e1e9be9df2d5dc6dbb21f7563710
fixed off-by-one bug

diff -r 87389311ba78 -r 69640564a394 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 13 10:10:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 13 10:10:43 2011 +0200
@@ -611,12 +611,14 @@
                                               atp_proof of
                    [] => result
                  | new_baddies =>
-                   let val blacklist = new_baddies @ blacklist in
-                     result
-                     |> maybe_run_slice blacklist (List.last actual_slices)
-                     |> iter < atp_blacklist_max_iters
-                        ? maybe_blacklist_facts_and_retry (iter + 1) blacklist
-                   end)
+                   if iter < atp_blacklist_max_iters - 1 then
+                     let val blacklist = new_baddies @ blacklist in
+                       result
+                       |> maybe_run_slice blacklist (List.last actual_slices)
+                       |> maybe_blacklist_facts_and_retry (iter + 1) blacklist
+                     end
+                   else
+                     result)
               | maybe_blacklist_facts_and_retry _ _ result = result
           in
             ((Symtab.empty, [], 0, Vector.fromList [], Symtab.empty),