# HG changeset patch
# User wenzelm
# Date 1565982138 -7200
# Node ID 9e87e978be5ed5c3d35af293ed9bb90f0331149e
# Parent  8bc7e54bead925372cf4811cdc62e896211bce03
clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;

diff -r 8bc7e54bead9 -r 9e87e978be5e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 16 14:01:51 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Aug 16 21:02:18 2019 +0200
@@ -177,6 +177,8 @@
     (string * class list list * class -> proof) -> sort list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_name: sort list -> term list -> term -> proof -> string
+  val get_id: sort list -> term list -> term -> proof ->
+    {serial: proof_serial, theory_name: string} option
 end
 
 structure Proofterm : PROOFTERM =
@@ -2183,10 +2185,12 @@
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
-        (PThm ({serial = i, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+        (PThm ({serial, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
           if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
-            let val Thm_Body {body = body', ...} = thm_body';
-            in (i, body' |> (a = "" andalso named) ? Future.map (publish i)) end
+            let
+              val Thm_Body {body = body', ...} = thm_body';
+              val i = if a = "" andalso named then proof_serial () else serial;
+            in (i, body' |> serial <> i ? Future.map (publish i)) end
           else new_prf ()
       | _ => new_prf ());
 
@@ -2221,13 +2225,24 @@
 
 (* approximative PThm name *)
 
-fun get_name shyps hyps prop prf =
+fun get_identity shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
     (case fst (strip_combt (fst (strip_combP prf))) of
-      PThm ({name, prop = prop', ...}, _) => if prop = prop' then name else ""
-    | _ => "")
+      PThm ({serial, theory_name, name, prop = prop', ...}, _) =>
+        if prop = prop'
+        then SOME {serial = serial, theory_name = theory_name, name = name} else NONE
+    | _ => NONE)
   end;
 
+fun get_name shyps hyps prop prf =
+  Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
+
+fun get_id shyps hyps prop prf =
+  (case get_identity shyps hyps prop prf of
+    NONE => NONE
+  | SOME {name = "", ...} => NONE
+  | SOME {serial, theory_name, ...} => SOME {serial = serial, theory_name = theory_name});
+
 end;
 
 structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
diff -r 8bc7e54bead9 -r 9e87e978be5e src/Pure/thm.ML
--- 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