proper maxidx: if x does not occur in A, its maxidx could get lost;

--- 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,