Synched up doc.lisp
fix for acl2(r) build
Fixed bug in *1* function generation that could cause raw Lisp type errors.

Quoting :doc note-7-0:

  A raw Lisp error could occur with [guard]-checking turned off,
  because type declarations were mistakenly left in the executable
  counterparts (so-called ``*1* functions'') when ACL2 processed
  function definitions. The following example shows how a type
  violation could occur in some Lisps (we saw this in SBCL but not in
  CCL, for example).

    (defun f (x)
      (declare (xargs :guard (natp x)))
      (let ((y (1+ x)))
        (declare (type (integer 0 *) y))
        y))
    (set-guard-checking nil)
    ; Possible raw Lisp error:
    ; "The value -2 is not of type UNSIGNED-BYTE."
    (f -3)

  Thanks to Jared Davis for sending us an example that brought this bug
  to our attention.
Synched doc.lisp