# HG changeset patch
# User wenzelm
# Date 1571598738 -7200
# Node ID 4c15217d6266019bb9560e3d901131b91d866e3a
# Parent  bd4d37edfee41e630bb06f33603f2dca1d905c4a
clarified signature: name of standard_proof is authentic, otherwise empty;

diff -r bd4d37edfee4 -r 4c15217d6266 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Oct 20 20:38:22 2019 +0200
+++ b/src/Pure/proofterm.ML	Sun Oct 20 21:12:18 2019 +0200
@@ -56,6 +56,7 @@
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   val unions_thms: thm Ord_List.T list -> thm Ord_List.T
   val no_proof_body: proof -> proof_body
+  val no_thm_names: proof -> proof
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
 
@@ -310,6 +311,14 @@
 fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
 val no_thm_body = thm_body (no_proof_body MinProof);
 
+fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
+  | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
+  | no_thm_names (prf % t) = no_thm_names prf % t
+  | no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2
+  | no_thm_names (PThm ({serial, pos, theory_name, name = _, prop, types}, thm_body)) =
+      PThm (thm_header serial pos theory_name "" prop types, thm_body)
+  | no_thm_names a = a;
+
 fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
   | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf)
   | no_thm_proofs (prf % t) = no_thm_proofs prf % t
@@ -2175,7 +2184,7 @@
     val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
 
     val consts = Sign.consts_of thy;
-    val xml = (typargs, (args, (prop', prf'))) |>
+    val xml = (typargs, (args, (prop', no_thm_names prf'))) |>
       let
         open XML.Encode Term_XML.Encode;
         val encode_vars = list (pair string typ);
diff -r bd4d37edfee4 -r 4c15217d6266 src/Pure/term.scala
--- a/src/Pure/term.scala	Sun Oct 20 20:38:22 2019 +0200
+++ b/src/Pure/term.scala	Sun Oct 20 21:12:18 2019 +0200
@@ -94,8 +94,7 @@
   case class PAxm(name: String, types: List[Typ]) extends Proof
   case class OfClass(typ: Typ, cls: Class) extends Proof
   case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
-  case class PThm(serial: Long, theory_name: String, approximative_name: String, types: List[Typ])
-    extends Proof
+  case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof
 
 
   /* type classes within the logic */