symbol-package-name-non-cl

(in-package "ACL2")

(define symbol-package-name-non-cl
  ((sym symbolp))
  :returns (pkg stringp)
  :enabled t
  :parents (std/basic)
  :short "The @(tsee symbol-package-name) of a symbol,
          but not @('"COMMON-LISP"')."
  :long (topstring (p "This function is just @(tsee symbol-package-name),
     except that it never returns @('"COMMON-LISP"'):
     if the @(tsee symbol-package-name) is @('"COMMON-LISP"'),
     we return @('"ACL2"') instead.")
    (p "Example:")
    (codeblock "ACL2 !>(symbol-package-name-non-cl 'car)"
      ""ACL2""
      "ACL2 !>(symbol-package-name 'car)"
      ""COMMON-LISP""
      "ACL2 !>")
    (p "This utility may be useful to obtain, from an existing symbol,
     a package name into whose package we want to intern a symbol
     for a new function name,
     which cannot be interned into the @('"COMMON-LISP"') package."))
  (fix-pkg (symbol-package-name sym)))