equal
deleted
inserted
replaced
103 |> sort_distinct (string_ord o apply2 #1); |
103 |> sort_distinct (string_ord o apply2 #1); |
104 |
104 |
105 val used = |
105 val used = |
106 Proofterm.fold_body_thms |
106 Proofterm.fold_body_thms |
107 (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) |
107 (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) |
108 (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
108 (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) |
109 Symtab.empty; |
109 Symtab.empty; |
110 |
110 |
111 fun is_unused a = not (Symtab.defined used a); |
111 fun is_unused a = not (Symtab.defined used a); |
112 |
112 |
113 (*groups containing at least one used theorem*) |
113 (*groups containing at least one used theorem*) |