The theorem export facility is very complex and has not been tested under all possible perverse conditions; it is likely to be reliable but not perfectly reliable. Problems I am aware of involve the treatment of numerals!
The variable binding context is a new addition (originally, the bracket construction was used only for constant functions and there were no bound variables at all). I suspect it of having bugs, and I also suspect that I will find awkwardnesses in it which will require me to revise it somewhat.