24 open Sledgehammer_Isar_Preplay |
24 open Sledgehammer_Isar_Preplay |
25 |
25 |
26 val slack = seconds 0.1 |
26 val slack = seconds 0.1 |
27 |
27 |
28 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step |
28 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step |
29 | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
29 | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...} |
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
30 (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) = |
31 (case get_preplay_outcome l of |
31 (case preplay_outcome l of |
32 Played time => |
32 Played time => |
33 let |
33 let |
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
34 fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth)) |
35 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
35 val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) |
36 |
36 |