74 | minimize_isar_step_dependencies _ _ step = step |
74 | minimize_isar_step_dependencies _ _ step = step |
75 |
75 |
76 fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = |
76 fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = |
77 let |
77 let |
78 fun process_steps [] = [] |
78 fun process_steps [] = [] |
79 | process_steps (steps as [Prove ([], [], l1, t1, subs1, facts1, meths1, comment1), |
79 | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), |
80 Prove ([Show], [], l2, t2, _, _, _, comment2)]) = |
80 Prove ([Show], [], l2, t2, _, _, _, comment2)]) = |
81 if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] |
81 if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] |
82 else steps |
82 else steps |
83 | process_steps (step :: steps) = step :: process_steps steps |
83 | process_steps (step :: steps) = step :: process_steps steps |
84 in |
84 in |