Another example is the [matroid intersection theorem][1], which is a rich source of min/max theorems in combinatorial optimzation.  For example, it includes your example ([Kőnig's theorem][2]) 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.  


  [1]: https://en.wikipedia.org/wiki/Matroid_intersection
  [2]: https://en.wikipedia.org/wiki/K%C5%91nig%27s_theorem_(graph_theory)