Enhanced variant of stobjs-in.
This returns the same result as stobjs-in,
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 stobjs-in+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'stobjs-in+)) (declare (ignorable __function__)) (if (not (function-symbolp fn wrld)) (raise "The symbol ~x0 does not name a function." fn) (b* ((result (stobjs-in fn wrld))) (if (symbol-listp result) result (raise "Internal error: ~ the STOBJS-IN property ~x0 of ~x1 ~ is not a true list of symbols." result fn))))))
(defthm symbol-listp-of-stobjs-in+ (b* ((result (stobjs-in+ fn wrld))) (symbol-listp result)) :rule-classes :rewrite)