# HG changeset patch
# User wenzelm
# Date 1532705262 -7200
# Node ID 0c568ec56f3705b1e04fda7b2122d404ce7a3545
# Parent  206966cbc2fcd9ffb8a8897dccc5d545ea95bba2
proper maxidx: if x does not occur in A, its maxidx could get lost;

diff -r 206966cbc2fc -r 0c568ec56f37 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 27 16:21:09 2018 +0200
+++ b/src/Pure/thm.ML	Fri Jul 27 17:27:42 2018 +0200
@@ -822,14 +822,14 @@
   \<And>x. A
 *)
 fun forall_intr
-    (ct as Cterm {t = x, T, sorts, ...})
-    (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
+    (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...})
+    (th as Thm (der, {maxidx = maxidx2, shyps, hyps, tpairs, prop, ...})) =
   let
     fun result a =
       Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
        {cert = join_certificate1 (ct, th),
         tags = [],
-        maxidx = maxidx,
+        maxidx = Int.max (maxidx1, maxidx2),
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
         tpairs = tpairs,