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 54124 d3c0cf737b55
parent 54112 9c0f464d1854
child 54142 5f3c1b445253 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 01:03:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 01:03:59 2013 +0200
@@ -570,7 +570,7 @@
     trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts");
     (if thres1 < 0.0 then
        facts
-     else if thres0 > 1.0 orelse thres0 > thres1 then
+     else if thres0 > 1.0 orelse thres0 > thres1 orelse max_facts <= 0 then
        []
      else
        relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
isabelle