# 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