changeset 70830 | 8f050cc0ec50 |
parent 70605 | 048cf2096186 |
--- a/src/Pure/Thy/thm_deps.ML Fri Oct 11 11:16:36 2019 +0200 +++ b/src/Pure/Thy/thm_deps.ML Fri Oct 11 15:36:32 2019 +0200 @@ -105,7 +105,7 @@ val used = Proofterm.fold_body_thms (fn {name = a, ...} => a <> "" ? Symtab.update (a, ())) - (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms))) + (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms))) Symtab.empty; fun is_unused a = not (Symtab.defined used a);