--- 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