# HG changeset patch
# User blanchet
# Date 1387126898 -3600
# Node ID dad9e53935243dfdbf6f6a10473db219bef0b294
# Parent  9b93f9117f8b7dfedbbd8cd5e83b3f705aad5602
more aggressive merging

diff -r 9b93f9117f8b -r dad9e5393524 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sun Dec 15 18:01:38 2013 +0100
@@ -76,18 +76,15 @@
     | _ => raise Fail "Sledgehammer_Compress: update_steps")
   end
 
-(* tries merging the first step into the second step *)
-fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meth1)))
+(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
       (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
-    if meth1 = meth2 then
-      let
-        val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
-        val gfs = union (op =) gfs1 gfs2
-      in
-        SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth1)))
-      end
-    else
-      NONE
+    let
+      val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
+      val gfs = union (op =) gfs1 gfs2
+    in
+      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+    end
   | try_merge _ _ = NONE
 
 val compress_degree = 2