clarified thm_id vs. thm_node/thm: retain theory_name;
support for thm_deps: expand unnamed nodes;

--- a/src/Pure/Thy/thm_deps.ML	Tue Aug 20 18:01:57 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Aug 20 18:39:33 2019 +0200
@@ -10,6 +10,7 @@
   val all_oracles: thm list -> Proofterm.oracle list
   val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
+  val thm_deps: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) list
   val thm_deps_cmd: theory -> thm list -> unit
   val unused_thms_cmd: theory list * theory list -> (string * thm) list
 end;
@@ -44,6 +45,22 @@
   in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
 
 
+(* thm_deps *)
+
+fun thm_deps thy =
+  let
+    val lookup = Global_Theory.lookup_thm_id thy;
+    fun deps (i, thm_node) res =
+      if Inttab.defined res i then res
+      else
+        let val thm_id = Proofterm.thm_id (i, thm_node) in
+          (case lookup thm_id of
+            SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res
+          | NONE => fold deps (Proofterm.thm_node_thms thm_node) res)
+        end;
+  in fn thm => fold deps (Thm.thm_deps thm) Inttab.empty |> Inttab.dest |> map #2 end;
+
+
 (* thm_deps_cmd *)
 
 fun thm_deps_cmd thy thms =

--- a/src/Pure/proofterm.ML	Tue Aug 20 18:01:57 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 18:39:33 2019 +0200
@@ -40,9 +40,11 @@
   val thm_body: proof_body -> thm_body
   val thm_body_proof_raw: thm_body -> proof
   val thm_body_proof_open: thm_body -> proof
+  val thm_node_theory_name: thm_node -> string
   val thm_node_name: thm_node -> string
   val thm_node_prop: thm_node -> term
   val thm_node_body: thm_node -> proof_body future
+  val thm_node_thms: thm_node -> thm list
   val join_thms: thm list -> proof_body list
   val consolidate: proof_body list -> unit
   val make_thm: thm_header -> thm_body -> thm
@@ -171,6 +173,7 @@
     (serial * proof_body future) list -> proof_body -> thm * proof
   val get_approximative_name: sort list -> term list -> term -> proof -> string
   type thm_id = {serial: serial, theory_name: string}
+  val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
 end
 
@@ -202,7 +205,8 @@
 and thm_body =
   Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
 and thm_node =
-  Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
+  Thm_Node of {theory_name: string, name: string, prop: term,
+    body: proof_body future, consolidate: unit lazy};
 
 type oracle = string * term option;
 val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
@@ -232,9 +236,11 @@
 fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
 
 fun rep_thm_node (Thm_Node args) = args;
+val thm_node_theory_name = #theory_name o rep_thm_node;
 val thm_node_name = #name o rep_thm_node;
 val thm_node_prop = #prop o rep_thm_node;
 val thm_node_body = #body o rep_thm_node;
+val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
 val thm_node_consolidate = #consolidate o rep_thm_node;
 
 fun join_thms (thms: thm list) =
@@ -244,15 +250,15 @@
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   #> Lazy.consolidate #> map Lazy.force #> ignore;
 
-fun make_thm_node name prop body =
-  Thm_Node {name = name, prop = prop, body = body,
+fun make_thm_node theory_name name prop body =
+  Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
     consolidate =
       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
         let val PBody {thms, ...} = Future.join body
         in consolidate (join_thms thms) end)};
 
-fun make_thm ({serial, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
-  (serial, make_thm_node name prop body);
+fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+  (serial, make_thm_node theory_name name prop body);
 
 
 (* proof atoms *)
@@ -341,8 +347,9 @@
 and proof_body (PBody {oracles, thms, proof = prf}) =
   triple (list (pair string (option term))) (list thm) proof (oracles, thms, prf)
 and thm (a, thm_node) =
-  pair int (triple string term proof_body)
-    (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
+  pair int (pair string (pair string (pair term proof_body)))
+    (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
+      (Future.join (thm_node_body thm_node))))));
 
 fun full_proof prf = prf |> variant
  [fn MinProof => ([], []),
@@ -394,8 +401,8 @@
   let val (a, b, c) = triple (list (pair string (option term))) (list thm) proof x
   in PBody {oracles = a, thms = b, proof = c} end
 and thm x =
-  let val (a, (b, c, d)) = pair int (triple string term proof_body) x
-  in (a, make_thm_node b c (Future.value d)) end;
+  let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair term proof_body))) x
+  in (a, make_thm_node b c d (Future.value e)) end;
 
 in
 
@@ -2145,10 +2152,10 @@
       if named orelse not (export_enabled ()) then no_export_proof
       else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1);
 
-    val thm = (i, make_thm_node name prop1 body');
+    val theory_name = Context.theory_long_name thy;
+    val thm = (i, make_thm_node theory_name name prop1 body');
 
-    val header =
-      thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
+    val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
     val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
     val head = PThm (header, thm_body);
     val proof =
@@ -2187,6 +2194,9 @@
 
 type thm_id = {serial: serial, theory_name: string};
 
+fun thm_id (serial, thm_node) : thm_id =
+  {serial = serial, theory_name = thm_node_theory_name thm_node};
+
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE

--- a/src/Pure/thm.ML	Tue Aug 20 18:01:57 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 20 18:39:33 2019 +0200
@@ -103,6 +103,7 @@
   val proof_of: thm -> proof
   val consolidate: thm list -> unit
   val future: thm future -> cterm -> thm
+  val thm_deps: thm -> Proofterm.thm Ord_List.T
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
   val derivation_id: thm -> Proofterm.thm_id option
@@ -990,10 +991,19 @@
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
 
+(*identified PThm node*)
 fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_id shyps hyps prop (proof_of thm)
     handle Proofterm.MIN_PROOF => NONE;
 
+(*dependencies of PThm node*)
+fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =
+      (case (derivation_id thm, thms) of
+        (SOME {serial = i, ...}, [(j, thm_node)]) =>
+          if i = j then Proofterm.thm_node_thms thm_node else thms
+      | _ => thms)
+  | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);
+
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let