# HG changeset patch
# User blanchet
# Date 1391468514 -3600
# Node ID e7029ee73a97658cb310ffed045b4f2a19b2cef4
# Parent  2bb02ba5d4b73ef8e61aae2e5dcf304d8a4ea22f
more liberal step merging

diff -r 2bb02ba5d4b7 -r e7029ee73a97 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 23:59:36 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Tue Feb 04 00:01:54 2014 +0100
@@ -88,7 +88,8 @@
         (case Lazy.force outcome of Played _ => true | _ => false)
       end
   in
-    inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful l2) meths2)
+    union (op =) meths1 meths2
+    |> filter (is_method_hopeful l1 andf is_method_hopeful l2)
   end
 
 fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))