# HG changeset patch
# User blanchet
# Date 1381964639 -7200
# Node ID d3c0cf737b55be5fcb8ea25beef40062f8f9c487
# Parent  271a8377656f2fb60f6c3a78d2848d0555a2652f
fast track -- avoid domain error in 0 case

diff -r 271a8377656f -r d3c0cf737b55 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- 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