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 (map Thm.proof_body_of thms) []; |
43 val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_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 |
54 val thms = |
54 val thms = |
55 fold (Facts.fold_static add_fact o PureThy.facts_of) thys [] |
55 fold (Facts.fold_static add_fact o PureThy.facts_of) thys [] |
56 |> sort_distinct (string_ord o pairself #1); |
56 |> sort_distinct (string_ord o pairself #1); |
57 |
57 |
58 val tab = Proofterm.fold_body_thms |
58 val tab = Proofterm.fold_body_thms |
59 (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) |
59 (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop)) |
60 (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; |
60 (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; |
61 fun is_unused (name, th) = |
61 fun is_unused (name, th) = |
62 not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); |
62 not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); |
63 |
63 |
64 (* groups containing at least one used theorem *) |
64 (* groups containing at least one used theorem *) |