Another example is the matroid intersection theorem, which is a rich source of min/max theorems in combinatorial optimzation. For example, it includes your example (Kőnig's theorem) as a special case.

There is an algorithmic proof of the matroid intersection theorem which runs in time polynomial in the sizes of the two matroids $M_1$ and $M_2$ and the running-time of the independence oracles for $M_1$ and $M_2$. Therefore, we get proofs which run in super-polynomial time whenever we have a matroid which cannot be described by an efficient independence oracle.

Another example is the matroid intersection theorem, which is a rich source of min/max theorems in combinatorial optimzation. For example, it includes your example (Kőnig's theorem) as a special case.

There is an algorithmic proof of the matroid intersection theorem which runs in time polynomial in $|E(M_1)|$, $|E(M_2)|$, and the running-times of the independence oracles for $M_1$ and $M_2$. Therefore, we get proofs which run in super-polynomial time whenever we have a matroid which cannot be described by an efficient independence oracle.