Made trivial improvement to time$ and our-time, and fixed "::prettyified-def" in books/defdata/base.lisp (GCL didn't like the repeated ":").

ACL2(h) "everything" regression based on very recent GCL 2.6.12pre now
passes.

Quoting a comment in (defxdoc note-7-0 ...) in
books/system/doc/acl2-doc.lisp:

; Modified our-time (hence, time$) to use essentially infinite right margins.
; This probably won't normally affect anyone, but is potentially useful if
; our-time is later extended to provide more information.