read-string-light

(defun read-string-light-fn
  (str pkg state)
  (declare (xargs :guard (and (stringp str) (or (null pkg) (stringp pkg)))
      :stobjs (state))
    (ignore str pkg))
  (prog2$ (er hard?
      'read-string-light
      "Raw lisp definition not installed?")
    (mv-let (err1 errmsg? state)
      (read-acl2-oracle state)
      (mv-let (err2 objects state)
        (read-acl2-oracle state)
        (if (or err1 err2)
          (mv (msg "Reading oracle failed.") nil state)
          (if errmsg?
            (mv errmsg? nil state)
            (mv nil objects state)))))))