1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 01:03:59 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Oct 17 01:03:59 2013 +0200
     1.3 @@ -570,7 +570,7 @@
     1.4      trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ " facts");
     1.5      (if thres1 < 0.0 then
     1.6         facts
     1.7 -     else if thres0 > 1.0 orelse thres0 > thres1 then
     1.8 +     else if thres0 > 1.0 orelse thres0 > thres1 orelse max_facts <= 0 then
     1.9         []
    1.10       else
    1.11         relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts