Fixed a couple of recently-introduced bugs in ACL2(h) that were preventing its build in SBCL.