# HG changeset patch
# User wenzelm
# Date 1566410930 -7200
# Node ID b85a12c2e2bff3e7ff54436bcb05e9acdc88ce3d
# Parent  79831e40e2be8ddefbe26770bc683edca6ee1047
proper graph traversal: avoid multiple visit of unnamed nodes;

diff -r 79831e40e2be -r b85a12c2e2bf src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Aug 21 17:32:44 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Wed Aug 21 20:08:50 2019 +0200
@@ -55,13 +55,16 @@
       else
         let val thm_id = Proofterm.thm_id (i, thm_node) in
           (case lookup thm_id of
-            SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res
-          | NONE => fold deps (Proofterm.thm_node_thms thm_node) res)
+            SOME thm_name =>
+              Inttab.update (i, SOME (thm_id, thm_name)) res
+          | NONE =>
+              Inttab.update (i, NONE) res
+              |> fold deps (Proofterm.thm_node_thms thm_node))
         end;
   in
     fn thm =>
-      fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty
-      |> Inttab.dest |> map #2
+      (fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty, [])
+      |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
   end;