We present a constructive procedure for extracting polynomial-time realizers from ineffective proofs of \prod {_2^0 }-theorems in feasible analysis. By ineffective proof we mean a proof which involves the non-computational principle weak K?nig?s lemma WKL, and by feasible analysis we mean Cook and Urquhart?s system CPV^\omega plus quantifier-free choice QF-AC. We shall also discuss the relation between the system CPV^\omega+QF-AC and Ferreira?s base theory for feasible analysis BTFA, forwhich \prod {_2^0 }-conservation of WKL has been non-constructively proven. This paper treats the case of weak K?nig?s lemma for trees defined by \prod {_1^0 }-formulas. Illustrating the applicability of CPV^\omega + QF-AC extended with this form of weak K?nig?s lemma, we indicate how to formalize the proof of the Heine/Borel covering lemma in this system. The main techniques used in the paper are G?del?s functional interpretation and a novel form of binary bar recursion.