--- a/src/Pure/thm.ML Fri Aug 16 14:01:51 2019 +0200
+++ b/src/Pure/thm.ML Fri Aug 16 21:02:18 2019 +0200
@@ -106,6 +106,7 @@
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
@@ -1004,6 +1005,9 @@
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