Yes, you are right: This is not what Craig's theorem says! It is enough to assume that the theorems are recursively enumerable. From this, it follows that there is an axiomatization where the axioms are recursive.
The key point is that I would find it a worthwhile addition to the paper to somehow make clear that "s proves S" is assumed to be decidable. Since you have done this: Thank you!
The key point is that I would find it a worthwhile addition to the paper to somehow make clear that "s proves S" is assumed to be decidable. Since you have done this: Thank you!