# 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 @@ \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,