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.