proper maxidx: if x does not occur in A, its maxidx could get lost;
authorwenzelm
Fri Jul 27 17:27:42 2018 +0200 (11 months ago)
changeset 686920c568ec56f37
parent 68691 206966cbc2fc
child 68693 a9bef20b1e47
proper maxidx: if x does not occur in A, its maxidx could get lost;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Jul 27 16:21:09 2018 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Jul 27 17:27:42 2018 +0200
     1.3 @@ -822,14 +822,14 @@
     1.4    \<And>x. A
     1.5  *)
     1.6  fun forall_intr
     1.7 -    (ct as Cterm {t = x, T, sorts, ...})
     1.8 -    (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
     1.9 +    (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...})
    1.10 +    (th as Thm (der, {maxidx = maxidx2, shyps, hyps, tpairs, prop, ...})) =
    1.11    let
    1.12      fun result a =
    1.13        Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
    1.14         {cert = join_certificate1 (ct, th),
    1.15          tags = [],
    1.16 -        maxidx = maxidx,
    1.17 +        maxidx = Int.max (maxidx1, maxidx2),
    1.18          shyps = Sorts.union sorts shyps,
    1.19          hyps = hyps,
    1.20          tpairs = tpairs,