effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
authorblanchet
Mon, 06 Jun 2011 23:11:14 +0200
changeset 43218 d6d084186df0
parent 43217 37d507be3014
child 43219 371cdc675cf9
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
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