Definition of the defun-inst macro.
Macro:
(defmacro defun-inst (fun sofun-inst &rest rest) (cons 'make-event-terse (cons (cons 'defun-inst-fn (cons (cons 'quote (cons fun 'nil)) (cons (cons 'quote (cons sofun-inst 'nil)) (cons (cons 'quote (cons rest 'nil)) (cons (cons 'cons (cons ''defun-inst (cons (cons 'quote (cons fun 'nil)) 'nil))) '(state)))))) 'nil)))
Macro:
(defmacro acl2::defun-inst (&rest args) (cons 'defun-inst args))