Quoting :doc note-6-5:

  Fixed a bug that was wrongly disallowing certain calls of exported
  functions for abstract stobjs (see [defabsstobj]). Thanks to Sol
  Swords for reporting this bug, supplying an example illustrating
  the bug, and suggesting a nice fix. A slight variant of his example
  is included in a comment in Community Books file
  system/doc/acl2-doc.lisp, form (defxdoc note-6-5 ...).


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