equal
deleted
inserted
replaced
77 else |
77 else |
78 (case group of |
78 (case group of |
79 NONE => I |
79 NONE => I |
80 | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty; |
80 | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty; |
81 val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') => |
81 val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') => |
82 if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] |
82 if not concealed andalso is_unused (a, th) then |
83 (Thm.get_kind th) andalso not concealed andalso is_unused (a, th) |
|
84 then |
|
85 (case group of |
83 (case group of |
86 NONE => ((a, th) :: thms, grps') |
84 NONE => ((a, th) :: thms, grps') |
87 | SOME grp => |
85 | SOME grp => |
88 (* do not output theorem if another theorem in group has been used *) |
86 (* do not output theorem if another theorem in group has been used *) |
89 if Inttab.defined used_groups grp then q |
87 if Inttab.defined used_groups grp then q |