Are there any natural recursively but not primitive-recursively axiomatized theories? In principle, we could have a recursively axiomatized theory for which the property numbers-an-axiom (even relative to some routine Gödel numbering scheme) is recursive but not primitive recursive. But are there any natural examples?
Of course, any such theory can be primitive-recursively reaxiomatized using Craig's trick. So we know that there can't be theories which are recursively axiomatizABLE but not primitive-recursively aziomatizABLE. But that's not the issue. The question is whether there is a theory T which when presented in a natural way requires open-ended searches to check whether a purported T-proof is indeed a proof according to that specification.  
[I couldn't think of one when I wrote the first edition of my Gödel book, and I still can't as I work on the second edition. But maybe I'm just being dim/ignorant!] 
 A: Here is another proposal. In this edition, the PS has been completely changed
Let $T_{ZFC}$ = arithmetical truths that $ZFC$ "knows about", i.e., the set of arithmetic sentences $\phi$ such that $ZFC$ proves $\phi^\omega$, where $\phi^\omega$ is the set-theoretical statement that expresses "$\phi$ holds in the von Neumann interpretation". 
$T_{ZFC}$ is an example of a natural r.e. theory whose overt axiomatization is not primitive recursive. Note that $T_{ZFC}$ is much stronger than $PA$, since includes all kinds of statements that are left undecided by $PA$, such as $Con(PA)$, $Con(PA + Con(PA)$, etc.
Moreover, one could argue that this theory is in some sense more natural than $PA$ since it is, implicitly, what mathematicians are really interested in.
Three notes:


*

*There are axiomatizations of $T_{ZFC}$ that do not use the Craig trick; see this FOM posting for more information.

*As observed by Kreisel, $T_{ZF}$ = $T_{ZFC + GCH}$ (the argument uses Gödel's constructible universe and absoluteness considerations).

*In light of Harvey Friedman's programme of unearthing the deep role of large cardinals in our knowledge of the finite realm, one can also consider natural variants $T_{ZFC^{+}}$, where $ZFC^{+}$ is the result of augmenting $ZFC$ with appropriate large cardinals.
P.S. Since the original question stipulated that the theory, when naturally presented,  be recursive, I offer the following (thanks to Emil Jeřábek and Joel Hamkins for helping to improve this suggestion).
Let $f_G$ be the Goodstein function, i.e., $f_G(m)=n$ iff the length of the Goodstein sequence starting at $m$ is $n$. Note that $f_G$ is recursive, but not primitive recursive. Then perhaps the equational theory of $(\Bbb{N}, 0, 1, +, f_G)$  is recursive but not primitive recursive.
Perhaps even the full theory of $(\Bbb{N}, 0, 1, +, f_G)$ is decidable (i.e., maybe Presburger arithmetic augmented with the Goodstein sequence is a decidable theory). 
A: Here is one proposal. 
Consider the natural theory of the Lindenbaum algebra of an undecidable theory $T$ (and natural examples of these abound). So the theory can refer to objects, which are sentences in the language of $T$, and there is an order relation axiomatized by $\varphi\leq \psi$ whenever $T\vdash\varphi\to\psi$. This is naturally a c.e. axiomatization of the theory, which can therefore be enumerated according a computable procedure, but this process does not seem to provide a primitive recursive axiomatization, except by means of the Craig's trick type reaxiomatization you mention. 
