# HG changeset patch
# User wenzelm
# Date 1571137891 -7200
# Node ID 69050518d4f33aa0feab9a7c257f55bb01433aac
# Parent  f2ce687bfa0a7ab5c99261a824cbb4f9f2a4b536
skip (somewhat pointless) shrink_proof more uniformly;

diff -r f2ce687bfa0a -r 69050518d4f3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Oct 15 11:48:25 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Oct 15 13:11:31 2019 +0200
@@ -2125,8 +2125,6 @@
     #> fold_rev (implies_intr_proof o snd) (#constraints ucontext)
   end;
 
-fun clean_proof thy = rew_proof thy #> shrink_proof;
-
 fun encode_export consts =
   let
     open XML.Encode Term_XML.Encode;
@@ -2199,8 +2197,8 @@
         (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 prop1) #> prune);
-    val open_proof = not named ? clean_proof thy;
+    fun publish i = map_proof_of (rew_proof thy #> tap (export thy i prop1) #> prune);
+    val open_proof = not named ? rew_proof thy;
 
     fun new_prf () =
       let