# HG changeset patch
# User wenzelm
# Date 1563967140 -7200
# Node ID be32cb8bfe2574b9f85aca89904c2b6656e6af25
# Parent  e8558735961a0c0686de8f002071ad2265f17e77
more accurate proof export;

diff -r e8558735961a -r be32cb8bfe25 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jul 24 13:18:15 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 24 13:19:00 2019 +0200
@@ -1727,22 +1727,22 @@
     fun prune prf1 =
       if Options.default_bool "prune_proofs" then MinProof else shrink_proof prf1;
 
-    fun publish i = clean_proof thy #> tap (export i) #> prune;
+    fun publish i = tap (export i) #> prune;
 
     fun new_prf () =
       let
         val i = serial ();
         val postproc =
           unconstrainT_body thy (atyp_map, constraints) #>
-          name <> "" ? map_proof_of (publish i);
+          name <> "" ? map_proof_of (clean_proof thy #> publish i);
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
-        (PThm (i, ((old_name, prop', NONE), body')), args') =>
-          if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'
-          then (i, body' |> name <> "" ? Future.map (map_proof_of (publish i)))
+        (PThm (i, ((a, prop', NONE), body')), args') =>
+          if (a = "" orelse a = name) andalso prop1 = prop' andalso args = args'
+          then (i, body' |> (a = "" andalso name <> "") ? Future.map (map_proof_of (publish i)))
           else new_prf ()
       | _ => new_prf ());
     val head = PThm (i, ((name, prop1, NONE), body'));