77 (case do_steps steps (rev updates) of |
77 (case do_steps steps (rev updates) of |
78 (steps, []) => steps |
78 (steps, []) => steps |
79 | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") |
79 | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") |
80 end |
80 end |
81 |
81 |
82 (* Tries merging the first step into the second step. *) |
82 fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1))) |
83 fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meths1))) |
83 (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) = |
84 (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meths2))) = |
|
85 let |
84 let |
86 val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 |
85 val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) |
87 val gfs = union (op =) gfs1 gfs2 |
86 val gfs = union (op =) gfs1 gfs2 |
|
87 val meths = fold_rev (insert (op =)) meths1 meths2 |
88 in |
88 in |
89 SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meths2))) |
89 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
90 end |
90 end |
91 | try_merge _ _ = NONE |
91 | try_merge _ _ = NONE |
92 |
92 |
93 val compress_degree = 2 |
93 val compress_degree = 2 |
94 val merge_timeout_slack = 1.2 |
94 val merge_timeout_slack = 1.2 |