equal
deleted
inserted
replaced
325 map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) |
325 map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) |
326 |
326 |
327 |
327 |
328 val add_labels_of_proof = |
328 val add_labels_of_proof = |
329 steps_of_proof #> fold_isar_steps |
329 steps_of_proof #> fold_isar_steps |
330 (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls |
330 (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls | _ => I)) |
331 | _ => I)) |
|
332 |
331 |
333 fun kill_useless_labels_in_proof proof = |
332 fun kill_useless_labels_in_proof proof = |
334 let |
333 let |
335 val used_ls = add_labels_of_proof proof [] |
334 val used_ls = add_labels_of_proof proof [] |
336 fun do_label l = if member (op =) used_ls l then l else no_label |
335 fun do_label l = if member (op =) used_ls l then l else no_label |