35 | keep_fastest_method_of_isar_step _ step = step |
35 | keep_fastest_method_of_isar_step _ step = step |
36 |
36 |
37 val slack = seconds 0.025 |
37 val slack = seconds 0.025 |
38 |
38 |
39 fun minimized_isar_step ctxt time |
39 fun minimized_isar_step ctxt time |
40 (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) = |
40 (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meth :: _, comment)) = |
41 let |
41 let |
42 val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00 |
42 val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00 |
43 |
43 |
44 fun mk_step_lfs_gfs lfs gfs = |
44 fun mk_step_lfs_gfs lfs gfs = |
45 Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) |
45 Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), [meth], comment) |
46 |
46 |
47 fun minimize_half _ min_facts [] time = (min_facts, time) |
47 fun minimize_half _ min_facts [] time = (min_facts, time) |
48 | minimize_half mk_step min_facts (fact :: facts) time = |
48 | minimize_half mk_step min_facts (fact :: facts) time = |
49 (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
49 (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth |
50 (mk_step (min_facts @ facts)) of |
50 (mk_step (min_facts @ facts)) of |