SYMBOL-PACKAGE-NAME

the name of the package of a symbol (a string) 
Major Section:  ACL2-BUILT-INS

WARNING: While symbol-package-name behaves properly on all ACL2 objects, it may give surprising results when called in raw Lisp. For more details see pkg-imports, in particular the discussion there of the "COMMON-LISP" package.

Completion Axiom (completion-of-symbol-package-name): 

(equal (symbol-package-name x)
       (if (symbolp x)
           (symbol-package-name x)
         ""))

Guard for (symbol-package-name x): 

(symbolp x)
Note: Symbol-package-name may diverge from the name of the symbol's package in raw Lisp, in the case that this package is the main Lisp package. For example, in GCL (symbol-package-name 'car) evaluates to "COMMON-LISP" even though the actual package name for the symbol, car, is "LISP".