clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;

--- a/src/Pure/Proof/reconstruct.ML	Tue Jul 23 12:16:02 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 23 19:04:56 2019 +0200
@@ -24,15 +24,6 @@
 fun message ctxt msg =
   if Config.get ctxt quiet_mode then () else writeln (msg ());
 
-fun vars_of t = map Var (rev (Term.add_vars t []));
-fun frees_of t = map Free (rev (Term.add_frees t []));
-
-fun forall_intr_vfs prop = fold_rev Logic.all
-  (vars_of prop @ frees_of prop) prop;
-
-fun forall_intr_vfs_prf prop prf = fold_rev Proofterm.forall_intr_proof'
-  (vars_of prop @ frees_of prop) prf;
-
 
 (* generate constraints for proof term *)
 
@@ -142,7 +133,7 @@
                 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
               | SOME Ts => (Ts, env));
             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
-              (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
+              (Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths =>
                 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
           in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
 
@@ -305,7 +296,7 @@
 
 fun prop_of_atom prop Ts = subst_atomic_types
   (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
-  (forall_intr_vfs prop);
+  (Proofterm.forall_intr_vfs prop);
 
 val head_norm = Envir.head_norm Envir.init;
 
@@ -366,7 +357,7 @@
                     val _ =
                       message ctxt (fn () =>
                         "Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop);
-                    val prf' = forall_intr_vfs_prf prop
+                    val prf' = Proofterm.forall_intr_vfs_prf prop
                       (reconstruct_proof ctxt prop (Proofterm.join_proof body));
                     val (maxidx', prfs', prf) = expand
                       (Proofterm.maxidx_proof prf' ~1) prfs prf'

--- a/src/Pure/proofterm.ML	Tue Jul 23 12:16:02 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 23 19:04:56 2019 +0200
@@ -149,6 +149,10 @@
     (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   val rew_proof: theory -> proof -> proof
 
+  val forall_intr_vfs: term -> term
+  val forall_intr_vfs_prf: term -> proof -> proof
+  val clean_proof: proof -> proof
+
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> sort list -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
@@ -1567,6 +1571,62 @@
 fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
 
 
+(* clean proof: expand unnamed PThm nodes *)
+
+local
+
+fun vars_of t = map Var (rev (Term.add_vars t []));
+fun frees_of t = map Free (rev (Term.add_frees t []));
+fun variables_of t = vars_of t @ frees_of t;
+
+in
+
+fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
+fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
+
+end;
+
+fun clean_proof prf =
+  let
+    fun clean maxidx prfs (AbsP (s, t, prf)) =
+          let val (maxidx', prfs', prf') = clean maxidx prfs prf
+          in (maxidx', prfs', AbsP (s, t, prf')) end
+      | clean maxidx prfs (Abst (s, T, prf)) =
+          let val (maxidx', prfs', prf') = clean maxidx prfs prf
+          in (maxidx', prfs', Abst (s, T, prf')) end
+      | clean maxidx prfs (prf1 %% prf2) =
+          let
+            val (maxidx', prfs', prf1') = clean maxidx prfs prf1;
+            val (maxidx'', prfs'', prf2') = clean maxidx' prfs' prf2;
+          in (maxidx'', prfs'', prf1' %% prf2') end
+      | clean maxidx prfs (prf % t) =
+          let val (maxidx', prfs', prf') = clean maxidx prfs prf
+          in (maxidx', prfs', prf' % t) end
+      | clean maxidx prfs (PThm (_, (("", prop, SOME Ts), body))) =
+          let
+            val (maxidx', prf, prfs') =
+              (case AList.lookup (op =) prfs prop of
+                NONE =>
+                  let
+                    val prf' = forall_intr_vfs_prf prop (join_proof body);
+                    val (maxidx', prfs', prf) = clean (maxidx_proof prf' ~1) prfs prf';
+                    val prfs'' = (prop, (maxidx', prf)) :: prfs';
+                  in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs'') end
+              | SOME (maxidx', prf) => (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs));
+            val tfrees = Term.add_tfrees prop [] |> rev;
+            val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
+              (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
+            val varify = map_type_tfree (fn p as (a, S) =>
+              if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
+          in
+            (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
+          end
+      | clean maxidx prfs prf = (maxidx, prfs, prf);
+
+    val maxidx = maxidx_proof prf ~1;
+  in norm_proof (Envir.empty maxidx) (#3 (clean maxidx [] prf)) end;
+
+
 
 (** promises **)
 
@@ -1657,19 +1717,22 @@
             (fn () => make_body0 (rew prf0))
         end;
 
+    fun export i prf1 =
+     (if Options.default_bool "export_proofs" then
+        Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
+          (Buffer.chunks
+            (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
+      else ();
+      if Options.default_bool "prune_proofs" then MinProof else prf1);
+
+    fun publish i = clean_proof #> export i #> shrink_proof;
+
     fun new_prf () =
       let
         val i = serial ();
-        fun export prf1 =
-         (if Options.default_bool "export_proofs" then
-            Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
-              (Buffer.chunks
-                (YXML.buffer_body (Term_XML.Encode.term (term_of_proof prf1)) Buffer.empty))
-          else ();
-          if Options.default_bool "prune_proofs" then MinProof else prf1);
         val postproc =
           unconstrainT_body thy (atyp_map, constraints) #>
-          map_proof_of (export #> shrink_proof);
+          name <> "" ? map_proof_of (publish i);
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
@@ -1677,7 +1740,7 @@
       (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')
+          then (i, body' |> name <> "" ? Future.map (map_proof_of (publish i)))
           else new_prf ()
       | _ => new_prf ());
     val head = PThm (i, ((name, prop1, NONE), body'));