# HG changeset patch
# User wenzelm
# Date 1566031082 -7200
# Node ID 10d41bf28b929bb01d7241223b0274bd34df84c6
# Parent  d18bd904c0fd99450af1532e21bd941e8787dbfb
clarified signature;

diff -r d18bd904c0fd -r 10d41bf28b92 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 16 21:50:57 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 17 10:38:02 2019 +0200
@@ -176,9 +176,9 @@
   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
     (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
+  val get_approximative_name: sort list -> term list -> term -> proof -> string
+  type thm_id = {serial: proof_serial, theory_name: string}
+  val get_id: sort list -> term list -> term -> proof -> thm_id option
 end
 
 structure Proofterm : PROOFTERM =
@@ -2223,7 +2223,7 @@
 end;
 
 
-(* approximative PThm name *)
+(* get PThm identity *)
 
 fun get_identity shyps hyps prop prf =
   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
@@ -2234,10 +2234,13 @@
     | _ => NONE)
   end;
 
-fun get_name shyps hyps prop prf =
+fun get_approximative_name shyps hyps prop prf =
   Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
 
-fun get_id shyps hyps prop prf =
+
+type thm_id = {serial: proof_serial, theory_name: string};
+
+fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE
   | SOME {name = "", ...} => NONE
diff -r d18bd904c0fd -r 10d41bf28b92 src/Pure/term.scala
--- a/src/Pure/term.scala	Fri Aug 16 21:50:57 2019 +0200
+++ b/src/Pure/term.scala	Sat Aug 17 10:38:02 2019 +0200
@@ -58,7 +58,7 @@
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class OfClass(typ: Typ, cls: String) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
-  case class PThm(serial: Long, theory_name: String, pseudo_name: String, types: List[Typ])
+  case class PThm(serial: Long, theory_name: String, approximative_name: String, types: List[Typ])
     extends Proof
 
 
diff -r d18bd904c0fd -r 10d41bf28b92 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 16 21:50:57 2019 +0200
+++ b/src/Pure/thm.ML	Sat Aug 17 10:38:02 2019 +0200
@@ -106,7 +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 derivation_id: thm -> Proofterm.thm_id option
   val raw_derivation_name: thm -> string
   val name_derivation: string * Position.T -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
@@ -999,11 +999,11 @@
 
 (*non-deterministic, depends on unknown promises*)
 fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
-  Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
+  Proofterm.get_approximative_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);
+  Proofterm.get_approximative_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);