1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sun Dec 15 18:01:38 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sun Dec 15 18:01:38 2013 +0100
     1.3 @@ -76,18 +76,15 @@
     1.4      | _ => raise Fail "Sledgehammer_Compress: update_steps")
     1.5    end
     1.6  
     1.7 -(* tries merging the first step into the second step *)
     1.8 -fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meth1)))
     1.9 +(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
    1.10 +fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
    1.11        (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
    1.12 -    if meth1 = meth2 then
    1.13 -      let
    1.14 -        val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
    1.15 -        val gfs = union (op =) gfs1 gfs2
    1.16 -      in
    1.17 -        SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth1)))
    1.18 -      end
    1.19 -    else
    1.20 -      NONE
    1.21 +    let
    1.22 +      val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
    1.23 +      val gfs = union (op =) gfs1 gfs2
    1.24 +    in
    1.25 +      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
    1.26 +    end
    1.27    | try_merge _ _ = NONE
    1.28  
    1.29  val compress_degree = 2