Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 67522 9e712280cc37
parent 65458 cf504b7a7aa7
child 69593 3dda49e08b9d 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -362,7 +362,7 @@
         Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp)))
     val (perfect, imperfect) = candidates
       |> sort (Real.compare o swap o apply2 snd)
-      |> take_prefix (fn (_, w) => w > 0.99999)
+      |> chop_prefix (fn (_, w) => w > 0.99999)
     val ((accepts, more_rejects), rejects) =
       chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   in
isabelle