91 fun is_unused (name, th) = case Symtab.lookup tab name of |
91 fun is_unused (name, th) = case Symtab.lookup tab name of |
92 NONE => true |
92 NONE => true |
93 | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th)); |
93 | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th)); |
94 (* groups containing at least one used theorem *) |
94 (* groups containing at least one used theorem *) |
95 val grps = fold (fn p as (_, thm) => if is_unused p then I else |
95 val grps = fold (fn p as (_, thm) => if is_unused p then I else |
96 case PureThy.get_group thm of |
96 case Thm.get_group thm of |
97 NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty; |
97 NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty; |
98 val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => |
98 val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => |
99 if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm) |
99 if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm) |
100 andalso is_unused p |
100 andalso is_unused p |
101 then |
101 then |
102 (case PureThy.get_group thm of |
102 (case Thm.get_group thm of |
103 NONE => (p :: thms, grps') |
103 NONE => (p :: thms, grps') |
104 | SOME grp => |
104 | SOME grp => |
105 (* do not output theorem if another theorem in group has been used *) |
105 (* do not output theorem if another theorem in group has been used *) |
106 if Symtab.defined grps grp then q |
106 if Symtab.defined grps grp then q |
107 (* output at most one unused theorem per group *) |
107 (* output at most one unused theorem per group *) |