acl2::deflist bugs

[bendyarm]

Not std::deflist or fty::deflist, but acl2::deflist.

This:

  (in-package "ACL2")
  (defun is3p (x) (equal x 3))
  (include-book "data-structures/deflist" :dir :system)
  (deflist is3-list-p (l) "recognizes lists of 3s" is3p)

works, but

  (defpkg "MYPACK" ())
  (in-package "MYPACK")
  (acl2::deflist is3-list-p2 (l) "recognizes lists of 3s" acl2::is3p)

does not:

    ACL2 Error in ACL2::TOP-LEVEL:  In the attempt to macroexpand the form
    (ACL2::DEFLIST IS3-LIST-P2 (L) "recognizes lists of 3s" ACL2::IS3P),
    evaluation of the macro body caused the error below.

    The guard for the function call 
    (ACL2::EXPLODE-NONNEGATIVE-INTEGER ACL2::N ACL2::PRINT-BASE ACL2::ANS),
    which is 
    (COMMON-LISP::AND (COMMON-LISP::INTEGERP ACL2::N)
                      (COMMON-LISP::>= ACL2::N 0)
                      (ACL2::PRINT-BASE-P ACL2::PRINT-BASE)),
    is violated by the arguments in the call 
    (ACL2::EXPLODE-NONNEGATIVE-INTEGER COMMON-LISP::NIL 10 COMMON-LISP::NIL).

Also,

  (acl2::deflist is3-list-p3 (acl2::l) "recognizes lists of 3s" acl2::is3p)

gets another different error:

    To verify that the 27 encapsulated events correctly extend the current
    theory we will evaluate them.  The theory thus constructed is only
    ephemeral.
    ...
    ACL2 Error in ( ACL2::DEFTHM IS3-LIST-P3-APPEND ...):  The symbol 
    LIST-TYPE-APPEND-LEMMA (in package "MYPACK") has neither a function  
    nor macro definition in ACL2.  Please define it; or perhaps you meant
    ACL2::LIST-TYPE-APPEND-LEMMA, which has the same name but is in a different
    package.
    ...