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.
move facts supplied with "add:" to the front, so that they get a better weight (SMT)
authorblanchet
Wed, 15 Dec 2010 16:42:06 +0100
changeset 41167 b05014180288
parent 41166 4b2a457b17e8
child 41168 f6f1ffd51d87
move facts supplied with "add:" to the front, so that they get a better weight (SMT)
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 15:13:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 16:42:06 2010 +0100
@@ -539,10 +539,8 @@
           relevant [] [] hopeful
         end
     fun add_facts ths accepts =
-      (facts |> filter ((member Thm.eq_thm ths
-                         andf (not o member (Thm.eq_thm o apsnd snd) accepts))
-                        o snd))
-      @ accepts
+      (facts |> filter (member Thm.eq_thm ths o snd)) @
+      (accepts |> filter_out (member Thm.eq_thm ths o snd))
       |> take max_relevant
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
isabelle