53 else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths; |
53 else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths; |
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 = |
59 (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop)) |
59 Proofterm.fold_body_thms |
60 (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; |
60 (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop)) |
|
61 (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty; |
61 fun is_unused (name, th) = |
62 fun is_unused (name, th) = |
62 not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); |
63 not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th)); |
63 |
64 |
64 (* groups containing at least one used theorem *) |
65 (* groups containing at least one used theorem *) |
65 val grps = fold (fn p as (_, thm) => if is_unused p then I else |
66 val grps = fold (fn p as (_, thm) => if is_unused p then I else |