Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
changeset 55323 253a029335a2
parent 55313 cddd94fb0e8d
child 55325 462ffd3b7065 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 21:29:46 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -84,7 +84,7 @@
         (case Lazy.force outcome of Played _ => true | _ => false)
       end
   in
-    union (op =) meths1 meths2
+    meths2 @ subtract (op =) meths2 meths1
     |> filter (is_method_hopeful l1 andf is_method_hopeful l2)
   end
isabelle