# HG changeset patch
# User wenzelm
# Date 1563916222 -7200
# Node ID 29d81b53c40bb410849bfb331fcaece4c2a5151a
# Parent  3c9f6aad092fd6220d6e2cc822412f396435b68d
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);

diff -r 3c9f6aad092f -r 29d81b53c40b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jul 23 19:07:28 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 23 23:10:22 2019 +0200
@@ -394,6 +394,7 @@
   | AbsP _ => false
   | op % _ => false
   | op %% _ => false
+  | MinProof => false
   | _ => true);
 
 fun compact_proof (prf % _) = compact_proof prf