call a function argument on the given list of arguments, no restrictions
Major Section:  ACL2-BUILT-INS

See oracle-apply, as we assume familiarity with that function. Oracle-apply-raw is a variant of oracle-apply that is untouchable, and hence requires a trust tag to remove the untouchability (see defttag and see remove-untouchable). Unlike oracle-apply, oracle-apply-raw simply calls the raw Lisp function funcall to compute the result, without restriction: the specified :guard is t, the function itself is applied (not its executable counterpart), there is no restriction for untouchable functions or return-last, and safe mode is not used. Thus, in general, oracle-apply-raw can be dangerous to use: any manner of error can occur!

As is the case for oracle-apply, the function symbol oracle-apply-raw is defined in :logic mode and is guard-verified. Oracle-apply-raw is logically defined to be oracle-apply; more precisely:

(oracle-apply-raw fn args state)
= {logical definition}
(ec-call (oracle-apply fn args state))