# HG changeset patch
# User wenzelm
# Date 1570804116 -7200
# Node ID 55e1dd3894ce93918ca9058086557191a0d52699
# Parent  8f050cc0ec501a1cbdd452044ff0716169250f68
tuned;

diff -r 8f050cc0ec50 -r 55e1dd3894ce src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Oct 11 15:36:32 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Oct 11 16:28:36 2019 +0200
@@ -1913,6 +1913,9 @@
 
 fun expand_proof thy thms prf =
   let
+    fun do_expand a prop =
+      exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms;
+
     fun expand maxidx prfs (AbsP (s, t, prf)) =
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
           in (maxidx', prfs', AbsP (s, t, prf')) end
@@ -1928,27 +1931,22 @@
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
           in (maxidx', prfs', prf' % t) end
       | expand maxidx prfs (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
-          if not (exists
-            (fn (b, NONE) => a = b
-              | (b, SOME prop') => a = b andalso prop = prop') thms)
-          then (maxidx, prfs, prf) else
-          let
-            val (maxidx', prf, prfs') =
-              (case AList.lookup (op =) prfs (a, prop) of
-                NONE =>
-                  let
-                    val prf' =
-                      thm_body_proof_open thm_body
-                      |> reconstruct_proof thy prop
-                      |> forall_intr_vfs_prf prop;
-                    val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf'
-                  in
-                    (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
-                      ((a, prop), (maxidx', prf)) :: prfs')
-                  end
-              | SOME (maxidx', prf) =>
-                  (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs));
-          in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end
+          if do_expand a prop then
+            let
+              val (maxidx', prfs', prf') =
+                (case AList.lookup (op =) prfs (a, prop) of
+                  NONE =>
+                    let
+                      val prf1 =
+                        thm_body_proof_open thm_body
+                        |> reconstruct_proof thy prop
+                        |> 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
+          else (maxidx, prfs, prf)
       | expand maxidx prfs prf = (maxidx, prfs, prf);
 
   in #3 (expand (maxidx_proof prf ~1) [] prf) end;