# HG changeset patch
# User blanchet
# Date 1307396608 -7200
# Node ID a6bda1a47c0a1b511bfba6dab3843436d486c5f4
# Parent  371cdc675cf93d043f1cae87d870061830b2b47e
removed confusing slicing logic

diff -r 371cdc675cf9 -r a6bda1a47c0a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:26:40 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:43:28 2011 +0200
@@ -156,13 +156,7 @@
   is_atp_installed (Proof_Context.theory_of ctxt)
 
 fun get_slices num_facts slicing slices =
-  (0 upto length slices - 1) ~~ slices
-  |> (if slicing andalso
-         exists (fn (_, (_, (max_facts, _))) => num_facts >= max_facts)
-                slices then
-        I
-      else
-        List.last #> single)
+  (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
 
 val metis_default_max_relevant = 20