proper theory context;
authorwenzelm
Tue, 20 Aug 2019 19:49:49 +0200
changeset 70596 3a7117c33742
parent 70595 2ae7e33c950f
child 70597 a896257a3f07
proper theory context;
src/Pure/Thy/thm_deps.ML
--- 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 *)