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.
fast track -- avoid domain error in 0 case
authorblanchet
Thu, 17 Oct 2013 01:03:59 +0200
changeset 54124 d3c0cf737b55
parent 54123 271a8377656f
child 54125 420b876ff1e2
fast track -- avoid domain error in 0 case
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML file | annotate | diff | comparison | revisions 
--- 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