# HG changeset patch
# User wenzelm
# Date 1566293928 -7200
# Node ID 35a4ef9c6d8094b3ae89aa471daca948d5de8875
# Parent  729f4d066d1aa8097a1263c08cb1793e7db35e6c
clarified modules;

diff -r 729f4d066d1a -r 35a4ef9c6d80 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Tue Aug 20 11:28:29 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Aug 20 11:38:48 2019 +0200
@@ -20,7 +20,16 @@
 (* oracles *)
 
 fun all_oracles thms =
-  Proofterm.all_oracles_of (map Thm.proof_body_of thms);
+  let
+    fun collect (PBody {oracles, thms, ...}) =
+      (if null oracles then I else apfst (cons oracles)) #>
+      (tap Proofterm.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 (Proofterm.thm_node_body thm_node)
+          in collect body (res, Inttab.update (i, ()) seen) end));
+    val bodies = map Thm.proof_body_of thms;
+  in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
 
 fun has_skip_proof thms =
   all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>);
diff -r 729f4d066d1a -r 35a4ef9c6d80 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 20 11:28:29 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 11:38:48 2019 +0200
@@ -43,6 +43,7 @@
   val thm_node_name: thm_node -> string
   val thm_node_prop: thm_node -> term
   val thm_node_body: thm_node -> proof_body future
+  val join_thms: pthm list -> proof_body list
   val consolidate: proof_body list -> unit
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms:
@@ -52,7 +53,6 @@
   val thm_ord: pthm ord
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
-  val all_oracles_of: proof_body list -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
   val no_proof_body: proof -> proof_body
   val no_thm_proofs: proof -> proof
@@ -290,17 +290,6 @@
 val unions_oracles = Ord_List.unions oracle_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
-fun all_oracles_of bodies =
-  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 (res, seen) =>
-        if Inttab.defined seen i then (res, seen)
-        else
-          let val body = Future.join (thm_node_body thm_node)
-          in collect body (res, Inttab.update (i, ()) seen) end));
-  in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
-
 fun approximate_proof_body prf =
   let
     val (oracles, thms) = fold_proof_atoms false