# HG changeset patch
# User wenzelm
# Date 1564233856 -7200
# Node ID d6a5301f9ffb6f404247e5f1483d603a7827c8a3
# Parent  617cd75fc3de2c1b6a237a2f88c4ba249bca2ff1
tuned;

diff -r 617cd75fc3de -r d6a5301f9ffb src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Jul 27 12:06:38 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Jul 27 15:24:16 2019 +0200
@@ -1700,9 +1700,6 @@
 
 val proof_serial = Counter.make ();
 
-
-(* publish *)
-
 local
 
 fun export thy i proof =
@@ -1715,17 +1712,10 @@
   if Options.default_bool "prune_proofs" then MinProof
   else shrink_proof proof;
 
-in
-
-fun publish thy i = clean_proof thy #> tap (export thy i) #> prune;
-
-end;
-
-
-(* PThm nodes *)
-
 fun prepare_thm_proof thy name shyps hyps concl promises body =
   let
+    val named = name <> "";
+
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
 
@@ -1741,12 +1731,13 @@
         (PBody {oracles = oracles0, thms = thms0,
           proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
 
+    fun publish i = map_proof_of (clean_proof thy #> tap (export thy i) #> prune);
+    val open_proof = not named ? (clean_proof thy #> shrink_proof);
+
     fun new_prf () =
       let
         val i = proof_serial ();
-        val postproc =
-          unconstrainT_body thy (atyp_map, constraints) #>
-          name <> "" ? map_proof_of (publish thy i);
+        val postproc = unconstrainT_body thy (atyp_map, constraints) #> named ? publish i;
       in (i, fulfill_proof_future thy promises postproc body0) end;
 
     val (i, body') =
@@ -1754,14 +1745,15 @@
       (case strip_combt (fst (strip_combP prf)) of
         (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 thy i)))
+          then (i, body' |> (a = "" andalso named) ? Future.map (publish i))
           else new_prf ()
       | _ => new_prf ());
 
-    val open_proof = if name = "" then clean_proof thy #> shrink_proof else I;
     val head = PThm (i, ((name, prop1, NONE, open_proof), body'));
   in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end;
 
+in
+
 fun thm_proof thy name shyps hyps concl promises body =
   let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body
   in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
@@ -1770,6 +1762,8 @@
   let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
   in (pthm, proof_combt' (head, args)) end;
 
+end;
+
 
 (* approximative PThm name *)