# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID e9fba9767d9202be2ae84331b9f697f0be23c5d6
# Parent  c402981f74c178c69bc666d0cb3cca73c0522e1e
merge proof methods

diff -r c402981f74c1 -r e9fba9767d92 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -79,14 +79,14 @@
     | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
   end
 
-(* Tries merging the first step into the second step. *)
-fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meths1)))
-      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meths2))) =
+fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1)))
+      (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) =
     let
-      val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
+      val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
       val gfs = union (op =) gfs1 gfs2
+      val meths = fold_rev (insert (op =)) meths1 meths2
     in
-      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meths2)))
+      SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
     end
   | try_merge _ _ = NONE