--- 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
--- 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
--- 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);