Modified the addition to :doc note-6-5 from the preceding check-in.
The change this time is that when a :program mode function calls the
*1* function for a :logic mode function because of the risk of an
ill-guarded stobj update, nevertheless an mbe call under that :logic
mode function will lead to evaluation of the :exec code, not the
:logic code.  As noted below, there is a (long) comment about this in
(defxdoc note-6-5 ...).

  Some evaluations of forms (mbe :logic L :exec E) are more efficient
  or avoid guard violations, by evaluation of the :exec form (E)
  instead of the :logic form (L). If the [mbe] call is in a
  :[program] mode function definition, the :exec code will be
  evaluated, where unlike before, this is true even when
  guard-checking is :all or :none (see [set-guard-checking]). If the
  mbe call is in a :[logic] mode function definition, the change is
  that the :exec code will be evaluated when there is a superior call
  of a :program mode function, except when guard-checking is :all or
  :none; this had failed to be the case in cases where there was an
  ``invariant-risk'' of ill-guarded stobj updates. However, there is
  no change in the case of safe-mode, which is used during evaluation
  of [defconst], [value-triple], and [defpkg] forms, and during
  macroexpansion: the :logic and :exec forms are still both evaluated
  and checked for equality. Thanks to Jared Davis for reporting this
  issue and for helpful chats about it. For more information, see the
  comment about ``mbe and invariant-risk'' in the form (defxdoc
  note-6-5 ...) in [community-books] file
  books/system/doc/acl2-doc.lisp.

Made additional minor change to raw-ev-fncall other than one in
support of the change above, that might help a bit with function
proclaiming.

Made additional minor tweaks to oneify-cltl-code in the process of
modifying it to support the change documented above.

Fixed a bug in with-base-10, which had used eq instead of eql to
compare numbers.

[Note: it remains to update doc.lisp to reflect
books/system/doc/acl2-doc.lisp changes.  I plan to fix that today.]


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1308 5d84a466-a78b-0930-a311-59b22171a541
Updated doc.lisp to match updates to books/system/doc/acl2-doc.lisp
(made in acl2-books revisions revision 2788 and 2789).

Removed a bit of dead code and adjusted a comment accordingly.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1309 5d84a466-a78b-0930-a311-59b22171a541