changeset 70596 | 3a7117c33742 |
parent 70595 | 2ae7e33c950f |
child 70602 | b85a12c2e2bf |
--- a/src/Pure/Thy/thm_deps.ML Tue Aug 20 18:39:33 2019 +0200 +++ b/src/Pure/Thy/thm_deps.ML Tue Aug 20 19:49:49 2019 +0200 @@ -58,7 +58,11 @@ SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res | NONE => fold deps (Proofterm.thm_node_thms thm_node) res) end; - in fn thm => fold deps (Thm.thm_deps thm) Inttab.empty |> Inttab.dest |> map #2 end; + in + fn thm => + fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty + |> Inttab.dest |> map #2 + end; (* thm_deps_cmd *)