# HG changeset patch
# User wenzelm
# Date 1227461876 -3600
# Node ID a87d27cc8498c92be7a972684f33717d4553c407
# Parent  c1c0e23ed0631b13eefb7dc68df7af1dfe4a35f5
tuned;

diff -r c1c0e23ed063 -r a87d27cc8498 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Nov 23 17:27:15 2008 +0100
+++ b/src/Pure/proofterm.ML	Sun Nov 23 18:37:56 2008 +0100
@@ -1242,9 +1242,9 @@
       map SOME (frees_of prop);
 
     val proof0 =
-      (if ! proofs = 2 then fold_rev implies_intr_proof hyps prf else MinProof)
-      |> rew_proof thy
-      |> (#4 o shrink_proof thy [] 0);
+      if ! proofs = 2 then
+        #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
+      else MinProof;
 
     fun new_prf () = (serial (), name, prop,
       Lazy.lazy (fn () => fulfill_proof thy (Lazy.force promises)