I'm currently trying to understand $E$-recursion theory, which is a generalization of classical recursion theory to arbitrary sets. One of the difficulties I'm having with understanding $E$-recursion is developing the right intuition for when a function is $E$-recursive. My intuition from classical recursion theory is that a function should be $E$-recursive precisely when it is $\Sigma_1$, but this breaks down in the $E$-recursive setting: while every $E$-recursive function is $\Sigma_1$, not every $\Sigma_1$ function is $E$-recursive.
This discrepancy is explained very nicely by van de Wiele's Theorem, which shows that a (total on $V$) function $f$ is $E$-recursive if and only if it is uniformly $\Sigma_1$-definable, by a formula with only finite ordinal parameters, over every $\Sigma_1$-admissible set $A$.
I'm currently reading a proof of this theorem in Sacks' book Higher Recursion Theory, but I'm interested in an apparent alternative proof he mentions. On page 325, there is the following paragraph:
"van de Wiele's proof is an application of proof-theoretic methods originated by Girard. Subsequently S. Simpson found a proof based on the compactness theorem for first order logic. The argument below is in the spirit of $E$-recursion and is extracted from Slaman . The latter approach appears to give more information than any of the others."
The original proof does not interest me particularly, since I don't know any proof theory, but the compactness-based proof sounds extremely interesting, and it sounds like the sort of thing that could help me get a better intuition for $E$-recursion. Unfortunately, Sacks does not say where Simpson's compactness-based proof can be found. I'd be very interested in seeing this proof, but my own searches of the literature have yielded nothing. So, my question is:
(*) What is Simpson's proof of van de Wiele's theorem, and where can I find it?
It has occurred to me that this may be unpublished; in that case, does anyone know an outline of how it would go?
Thanks in advance!