# HG changeset patch
# User wenzelm
# Date 1565942687 -7200
# Node ID 33749040b6f87e1ce33104d38491eafe522ec3ff
# Parent  011196c029e155da26dcd8d978cc5b45fd79b656
clarified derivation_name vs. raw_derivation_name;

diff -r 011196c029e1 -r 33749040b6f8 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Aug 15 21:46:43 2019 +0200
+++ b/src/Pure/global_theory.ML	Fri Aug 16 10:04:47 2019 +0200
@@ -128,7 +128,7 @@
       No_Name_Flags => thm
     | Name_Flags {pre, official} =>
         thm
-        |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
+        |> (official andalso (not pre orelse Thm.raw_derivation_name thm = "")) ?
             Thm.name_derivation (name, pos)
         |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
diff -r 011196c029e1 -r 33749040b6f8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Aug 15 21:46:43 2019 +0200
+++ b/src/Pure/thm.ML	Fri Aug 16 10:04:47 2019 +0200
@@ -106,6 +106,7 @@
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
+  val raw_derivation_name: thm -> string
   val name_derivation: string * Position.T -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
@@ -996,9 +997,13 @@
   Proofterm.compact_proof (Proofterm.proof_of body);
 
 (*non-deterministic, depends on unknown promises*)
-fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   Proofterm.get_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);
+
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let