# HG changeset patch
# User blanchet
# Date 1289035508 -3600
# Node ID 0d0acdf068b85ca8d9b5c99002361926cb20bf77
# Parent  cb9fd7dd641c793c9cb9de8bfa09e07fa95b8e0f
always honor the max relevant constraint

diff -r cb9fd7dd641c -r 0d0acdf068b8 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Nov 06 00:10:32 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Nov 06 10:25:08 2010 +0100
@@ -520,6 +520,7 @@
                          andf (not o member (Thm.eq_thm o apsnd snd) accepts))
                         o snd))
       @ accepts
+      |> take max_relevant
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
           |> iter 0 max_relevant threshold0 goal_const_tab []