# HG changeset patch
# User wenzelm
# Date 1584558290 -3600
# Node ID c2884545c846025de2da96bb305d3aa55d9b7fc7
# Parent  391ea80ff27c443ab00b33f55a1ea69c15ffbd05
slightly more explicit error, without going into the graph of proof futures;

diff -r 391ea80ff27c -r c2884545c846 src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Wed Mar 18 18:06:36 2020 +0100
+++ b/src/Pure/thm_deps.ML	Wed Mar 18 20:04:50 2020 +0100
@@ -42,7 +42,11 @@
     fun prt_oracle (ora, NONE) = prt_ora ora
       | prt_oracle (ora, SOME prop) =
           prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
-  in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
+    val oracles =
+      (case try all_oracles thms of
+        SOME oracles => oracles
+      | NONE => error "Malformed proofs")
+  in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end;
 
 
 (* thm_deps *)
@@ -70,8 +74,12 @@
 fun pretty_thm_deps thy thms =
   let
     val ctxt = Proof_Context.init_global thy;
+    val deps =
+      (case try (thm_deps thy) thms of
+        SOME deps => deps
+      | NONE => error "Malformed proofs");
     val items =
-      map #2 (thm_deps thy thms)
+      map #2 deps
       |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
       |> sort_by (#2 o #1)
       |> map (fn ((marks, xname), i) =>