(module acl2-app mzscheme
  (require "defun-state.scm")
  (require-for-syntax "syntax-checks.scm")
  (provide acl2-app)
  (require-for-template mzscheme)
 
  (define-syntax (acl2-app stx)
    (syntax-case stx ()
      [(_ (unbox id) args ...) ;; generated by unit linking
       #'(#%app (unbox id) args ...)]
      [(_ id args ...)
       (and (identifier? #'id) (not (legal-constant-name? #'id)))
       #'(#%app id args ...)]
      [(_ id args ...)
       (legal-constant-name? #'id)
       (raise-syntax-error #f "This is a constant name, but we expected a function name." stx #'id)]
      [(_ something args ...)
       (raise-syntax-error #f "Expected the name of a function here" stx #'something)]))
  )