merge proof methods
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55246e9fba9767d92
parent 55245 c402981f74c1
child 55247 4aa3e1c6222c
merge proof methods
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -79,14 +79,14 @@
     1.4      | _ => raise Fail "Sledgehammer_Isar_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), meths1)))
     1.9 -      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meths2))) =
    1.10 +fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1)))
    1.11 +      (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) =
    1.12      let
    1.13 -      val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
    1.14 +      val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
    1.15        val gfs = union (op =) gfs1 gfs2
    1.16 +      val meths = fold_rev (insert (op =)) meths1 meths2
    1.17      in
    1.18 -      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meths2)))
    1.19 +      SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
    1.20      end
    1.21    | try_merge _ _ = NONE
    1.22