author blanchet Sun Feb 02 20:53:51 2014 +0100 (2014-02-02) changeset 55246 e9fba9767d92 parent 55245 c402981f74c1 child 55247 4aa3e1c6222c
merge proof methods
```     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
```