Construction of a real closure

Is there a reference for the fact that a countable decidably ordered field has a constructable (and decidably ordered) real closure? Maybe 20 years ago, an undergraduate did a project under my supervision proving exactly that (although the proofs are not constructive). While I don't think it would prove feasible for actual computation, the fact that it exists is interesting. Finally, I have looked more closely at it and if it is not known, I think it publishable. Unfortunately, the student (who was a Commonwealth Fellow at Cambridge) lost interest in math and is doing other things. But I think I know how to get in touch with him. Michael