# HG changeset patch
# User wenzelm
# Date 1566233269 -7200
# Node ID 10dd61d9357a87a040cd41ff035f7cf1e287595f
# Parent  d94456876f2d3d5900588d241f1be39642eebb5b
tuned;

diff -r d94456876f2d -r 10dd61d9357a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 17 19:04:03 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Aug 19 18:47:49 2019 +0200
@@ -302,11 +302,11 @@
   let
     fun collect (PBody {oracles, thms, ...}) =
       (if null oracles then I else apfst (cons oracles)) #>
-      (tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
-        if Inttab.defined seen i then (x, seen)
+      (tap join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
+        if Inttab.defined seen i then (res, seen)
         else
           let val body = Future.join (thm_node_body thm_node)
-          in collect body (x, Inttab.update (i, ()) seen) end));
+          in collect body (res, Inttab.update (i, ()) seen) end));
   in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
 
 fun approximate_proof_body prf =