src/Pure/thm.ML

   val consolidate: thm list -> unit
   val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
+  val derivation_id: thm -> {serial: proof_serial, theory_name: string} option
   val raw_derivation_name: thm -> string
   val name_derivation: string * Position.T -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm

   Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
 
 (*deterministic name of finished proof*)
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_name shyps hyps prop (proof_of thm);
+
+fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
+  Proofterm.get_id shyps hyps prop (proof_of thm);
 
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let
       val thy = theory_of_thm thm;