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) is a symbol in that package whose symbol-name is the value of constant *pkg-witness-name*. Logically, this is the case even if the package is not currently known to ACL2. However, if pkg-witness is called on a string that is not the name of a package known to ACL2, a hard Lisp error will result.

(Pkg-witness pkg) has a guard of (and (stringp pkg) (not (equal pkg ""))). If pkg is not a string, then (pkg-witness pkg) is equal to (pkg-witness "ACL2")