PKG-WITNESS

return a specific symbol in the indicated package 
Major Section:  PROGRAMMING

For any string pkg that names a package currently known to ACL2, (pkg-witness pkg) evaluates to a symbol in that package whose symbol-name is the value of constant *pkg-witness-name*.

(Pkg-witness pkg) has a guard of (stringp pkg). However, if pkg-witness is called on an argument that is not the name of a package known to ACL2, a hard Lisp error will result.