Enhanced variant of ubody.
This returns the same result as ubody,
but it includes a run-time check (which should always succeed) on the result
that allows us to prove the return type theorem
without strengthening the guard on
(defun ubody+ (fn wrld) (declare (xargs :guard (and (pseudo-termfnp fn) (plist-worldp wrld)))) (let ((__function__ 'ubody+)) (declare (ignorable __function__)) (if (and (symbolp fn) (not (function-symbolp fn wrld))) (raise "The symbol ~x0 does not name a function." fn) (b* ((result (ubody fn wrld))) (if (pseudo-termp result) result (raise "Internal error: ~ the unnormalized body ~x0 of ~x1 is not a pseudo-term." result fn))))))
(defthm pseudo-termp-of-ubody+ (b* ((body (ubody+ fn wrld))) (pseudo-termp body)) :rule-classes :rewrite)