# HG changeset patch
# User blanchet
# Date 1307394674 -7200
# Node ID d6d084186df02cdd04c6e62a69898f8fba3f6656
# Parent  37d507be30143dbce9cbab7e142bb164e2294e9a
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake

diff -r 37d507be3014 -r d6d084186df0 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 22:03:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:11:14 2011 +0200
@@ -158,7 +158,7 @@
 fun get_slices num_facts slicing slices =
   (0 upto length slices - 1) ~~ slices
   |> (if slicing andalso
-         exists (fn (_, (_, (max_facts, _))) => max_facts < num_facts)
+         exists (fn (_, (_, (max_facts, _))) => num_facts >= max_facts)
                 slices then
         I
       else