diff -r c92443e8d724 -r 7714971a58b5 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Aug 17 11:52:47 2019 +0200
+++ b/src/Pure/Pure.thy	Sat Aug 17 12:44:22 2019 +0200
@@ -84,7 +84,7 @@
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
-    "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
+    "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings"
     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
   and "print_state" :: diag
@@ -1307,6 +1307,15 @@
         Thm_Deps.thm_deps (Toplevel.theory_of st)
           (Attrib.eval_thms (Toplevel.context_of st) args))));
 
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>
+    "print all oracles used in theorems (full graph of transitive dependencies)"
+    (Parse.thms1 >> (fn args =>
+      Toplevel.keep (fn st =>
+        let
+          val ctxt = Toplevel.context_of st;
+          val thms = Attrib.eval_thms ctxt args;
+        in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end)));
 
 val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name);