equal
deleted
inserted
replaced
38 dir = space_implode "/" (session @ prefix), |
38 dir = space_implode "/" (session @ prefix), |
39 unfold = false, |
39 unfold = false, |
40 path = "", |
40 path = "", |
41 parents = parents}; |
41 parents = parents}; |
42 in cons entry end; |
42 in cons entry end; |
43 val deps = Proofterm.fold_body_thms add_dep (Future.joins (map Thm.future_body_of thms)) []; |
43 val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; |
44 in Present.display_graph (sort_wrt #ID deps) end; |
44 in Present.display_graph (sort_wrt #ID deps) end; |
45 |
45 |
46 |
46 |
47 (* unused_thms *) |
47 (* unused_thms *) |
48 |
48 |
64 |> sort_distinct (string_ord o pairself #1); |
64 |> sort_distinct (string_ord o pairself #1); |
65 |
65 |
66 val used = |
66 val used = |
67 Proofterm.fold_body_thms |
67 Proofterm.fold_body_thms |
68 (fn (a, _, _) => a <> "" ? Symtab.update (a, ())) |
68 (fn (a, _, _) => a <> "" ? Symtab.update (a, ())) |
69 (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms))) |
69 (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
70 Symtab.empty; |
70 Symtab.empty; |
71 |
71 |
72 fun is_unused a = not (Symtab.defined used a); |
72 fun is_unused a = not (Symtab.defined used a); |
73 |
73 |
74 (* groups containing at least one used theorem *) |
74 (* groups containing at least one used theorem *) |