By default, ACL2 causes an error when either of the keywords :hints or :measure is supplied in an xargsdeclare form
for a :logic mode non-recursive definition. That restriction
also applies to :program mode definitions in the case of
:measure. This behavior can be defeated with
(set-bogus-defun-hints-ok t), or if you still want to see a warning in
such cases, (set-bogus-defun-hints-ok :warn). This utility should
perhaps be called set-bogus-defun-hints-and-measures-ok, but we retain
its original name (from when it did not deal with bogus measures).
