# HG changeset patch
# User wenzelm
# Date 1570804372 -7200
# Node ID 86e272f26afcc601227567dc581dd406fd9426c8
# Parent  55e1dd3894ce93918ca9058086557191a0d52699
tuned;

diff -r 55e1dd3894ce -r 86e272f26afc src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Oct 11 16:28:36 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 11 16:32:52 2019 +0200
@@ -1943,9 +1943,10 @@
                         |> forall_intr_vfs_prf prop;
                       val (maxidx1, prfs1, prf2) = expand (maxidx_proof prf1 ~1) prfs prf1
                       val prfs2 = ((a, prop), (maxidx1, prf2)) :: prfs1;
-                    in (maxidx1, prfs2, incr_indexes (maxidx + 1) prf2) end
-                | SOME (maxidx1, prf1) => (maxidx1, prfs, incr_indexes (maxidx + 1) prf1));
-            in (maxidx' + maxidx + 1, prfs', app_types (maxidx + 1) prop Ts prf') end
+                    in (maxidx1, prfs2, prf2) end
+                | SOME (maxidx1, prf1) => (maxidx1, prfs, prf1));
+              val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts;
+            in (maxidx' + maxidx + 1, prfs', prf'') end
           else (maxidx, prfs, prf)
       | expand maxidx prfs prf = (maxidx, prfs, prf);