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.
always honor the max relevant constraint
authorblanchet
Sat, 06 Nov 2010 10:25:08 +0100
changeset 40408 0d0acdf068b8
parent 40388 cb9fd7dd641c
child 40409 3642dc3b72e8
always honor the max relevant constraint
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML file | annotate | diff | comparison | revisions 
--- 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 []
isabelle