# HG changeset patch
# User wenzelm
# Date 1566033800 -7200
# Node ID 5d6e9c65ea6779a209299a70c0e7b1da57a9cfb4
# Parent  038ed9b76c2b6e4caced755244889eafbe9127e7
clarified signature;

diff -r 038ed9b76c2b -r 5d6e9c65ea67 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 17 11:13:16 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 17 11:23:20 2019 +0200
@@ -7,6 +7,7 @@
 
 signature THM_DEPS =
 sig
+  val all_oracles: thm list -> Proofterm.oracle list
   val thm_deps: theory -> thm list -> unit
   val unused_thms: theory list * theory list -> (string * thm) list
 end;
@@ -14,6 +15,12 @@
 structure Thm_Deps: THM_DEPS =
 struct
 
+(* oracles *)
+
+fun all_oracles thms =
+  Proofterm.all_oracles_of (map Thm.proof_body_of thms);
+
+
 (* thm_deps *)
 
 fun thm_deps thy thms =
diff -r 038ed9b76c2b -r 5d6e9c65ea67 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 17 11:13:16 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 17 11:23:20 2019 +0200
@@ -61,7 +61,7 @@
   val thm_ord: pthm * pthm -> order
   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 -> oracle 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
@@ -317,7 +317,7 @@
 val unions_oracles = Ord_List.unions oracle_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
-val all_oracles_of =
+fun all_oracles_of bodies =
   let
     fun collect (PBody {oracles, thms, ...}) =
       (if null oracles then I else apfst (cons oracles)) #>
@@ -326,7 +326,7 @@
         else
           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;
+  in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
 
 fun approximate_proof_body prf =
   let