src/Pure/Thy/thm_deps.ML
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);