Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed confusing slicing logic
authorblanchet
Mon, 06 Jun 2011 23:43:28 +0200
changeset 43220 a6bda1a47c0a
parent 43219 371cdc675cf9
child 43221 2c88166938eb
removed confusing slicing logic
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle