# HG changeset patch
# User wenzelm
# Date 1565339454 -7200
# Node ID c65ccd813f4d31d99d0f9926aebc5dd65c6915d7
# Parent  8cac53925407f363974180a0fa8d272bdb2a43c4
proper treatment of body oracles, outside of recursion into thms graph;

diff -r 8cac53925407 -r c65ccd813f4d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Aug 08 12:18:27 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Aug 09 10:30:54 2019 +0200
@@ -288,13 +288,12 @@
 val all_oracles_of =
   let
     fun collect (PBody {oracles, thms, ...}) =
-      tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
+      (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)
         else
-          let
-            val body = Future.join (thm_node_body thm_node);
-            val (x', seen') = collect body (x, Inttab.update (i, ()) seen);
-          in (if null oracles then x' else oracles :: x', seen') end);
+          let val body = Future.join (thm_node_body thm_node)
+          in collect body (x, Inttab.update (i, ()) seen) end));
   in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
 
 fun approximate_proof_body prf =