This change was necessary to avoid the following error--at least using
ACL2 versions 7.0 and 8.0 which were the only ones tried.
ACL2 Error in ( DEFUN REWRITE/DEFINE+ ...): It is illegal to supply
a measure for a non-recursive function, as has been done for REWRITE/DEFINE+.
To avoid this error, see :DOC set-bogus-measure-ok.
This change was necessary to avoid the following error--at least using ACL2 versions 7.0 and 8.0 which were the only ones tried.
ACL2 Error in ( DEFUN REWRITE/DEFINE+ ...): It is illegal to supply a measure for a non-recursive function, as has been done for REWRITE/DEFINE+. To avoid this error, see :DOC set-bogus-measure-ok.