src/Pure/thm.ML

      B
   -------
   A \<Longrightarrow> B
 *)
 fun implies_intr
-    (ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...})
-    (th as Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...})) =
+    (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...})
+    (th as Thm (der, {maxidx = maxidx2, hyps, shyps, tpairs, prop, ...})) =
   if T <> propT then
     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   else
     Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
      {cert = join_certificate1 (ct, th),
       tags = [],
-      maxidx = Int.max (maxidxA, maxidx),
+      maxidx = Int.max (maxidx1, maxidx2),
       shyps = Sorts.union sorts shyps,
       hyps = remove_hyps A hyps,
       tpairs = tpairs,
       prop = Logic.mk_implies (A, prop)});
 

   ------------
         B
 *)
 fun implies_elim thAB thA =
   let
-    val Thm (derA, {maxidx = maxA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,
+    val Thm (derA, {maxidx = maxidx1, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,
       prop = propA, ...}) = thA
-    and Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...}) = thAB;
+    and Thm (der, {maxidx = maxidx2, hyps, shyps, tpairs, prop, ...}) = thAB;
     fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   in
     case prop of
       Const ("Pure.imp", _) $ A $ B =>
         if A aconv propA then
           Thm (deriv_rule2 (curry Proofterm.%%) der derA,
            {cert = join_certificate2 (thAB, thA),
             tags = [],
-            maxidx = Int.max (maxA, maxidx),
+            maxidx = Int.max (maxidx1, maxidx2),
             shyps = Sorts.union shypsA shyps,
             hyps = union_hyps hypsA hyps,
             tpairs = union_tpairs tpairsA tpairs,
             prop = B})
         else err ()

   \<And>x. A
   ------
   A[t/x]
 *)
 fun forall_elim
-    (ct as Cterm {t, T, maxidx = maxt, sorts, ...})
-    (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
+    (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...})
+    (th as Thm (der, {maxidx = maxidx2, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
     Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
       if T <> qary then
         raise THM ("forall_elim: type mismatch", 0, [th])
       else
         Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
          {cert = join_certificate1 (ct, th),
           tags = [],
-          maxidx = Int.max (maxidx, maxt),
+          maxidx = Int.max (maxidx1, maxidx2),
           shyps = Sorts.union sorts shyps,
           hyps = hyps,
           tpairs = tpairs,
           prop = Term.betapply (A, t)})
   | _ => raise THM ("forall_elim: not quantified", 0, [th]));

   ------------------
        t1 \<equiv> t2
 *)
 fun transitive th1 th2 =
   let
-    val Thm (der1, {maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,
+    val Thm (der1, {maxidx = maxidx1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,
       prop = prop1, ...}) = th1
-    and Thm (der2, {maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
+    and Thm (der2, {maxidx = maxidx2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
       prop = prop2, ...}) = th2;
     fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
   in
     case (prop1, prop2) of
       ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
         if not (u aconv u') then err "middle term"
         else
           Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
-            maxidx = Int.max (max1, max2),
+            maxidx = Int.max (maxidx1, maxidx2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,
             prop = eq $ t1 $ t2})
      | _ =>  err "premises"

   -------------
     f t \<equiv> g u
 *)
 fun combination th1 th2 =
   let
-    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
+    val Thm (der1, {maxidx = maxidx1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
       prop = prop1, ...}) = th1
-    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
+    and Thm (der2, {maxidx = maxidx2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
       prop = prop2, ...}) = th2;
     fun chktypes fT tT =
       (case fT of
         Type ("fun", [T1, _]) =>
           if T1 <> tT then

        Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
         (chktypes fT tT;
           Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
-            maxidx = Int.max (max1, max2),
+            maxidx = Int.max (maxidx1, maxidx2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,
             prop = Logic.mk_equals (f $ t, g $ u)}))
      | _ => raise THM ("combination: premises", 0, [th1, th2]))

   ----------------
        A \<equiv> B
 *)
 fun equal_intr th1 th2 =
   let
-    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
+    val Thm (der1, {maxidx = maxidx1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
       prop = prop1, ...}) = th1
-    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
+    and Thm (der2, {maxidx = maxidx2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
       prop = prop2, ...}) = th2;
     fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
   in
     (case (prop1, prop2) of
       (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
         if A aconv A' andalso B aconv B' then
           Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
-            maxidx = Int.max (max1, max2),
+            maxidx = Int.max (maxidx1, maxidx2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,
             prop = Logic.mk_equals (A, B)})
         else err "not equal"

   ---------
       B
 *)
 fun equal_elim th1 th2 =
   let
-    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1,
+    val Thm (der1, {maxidx = maxidx1, shyps = shyps1, hyps = hyps1,
       tpairs = tpairs1, prop = prop1, ...}) = th1
-    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2,
+    and Thm (der2, {maxidx = maxidx2, shyps = shyps2, hyps = hyps2,
       tpairs = tpairs2, prop = prop2, ...}) = th2;
     fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
   in
     (case prop1 of
       Const ("Pure.eq", _) $ A $ B =>
         if prop2 aconv A then
           Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
            {cert = join_certificate2 (th1, th2),
             tags = [],
-            maxidx = Int.max (max1, max2),
+            maxidx = Int.max (maxidx1, maxidx2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,
             prop = B})
         else err "not equal"