set the default measure function symbol
Major Section:  EVENTS

(set-measure-function nqthm::count)
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

General Form:
(set-measure-function name)
where name is a function symbol of one argument. This macro is equivalent to (table acl2-defaults-table :measure-function 'name), which is also an event (see table), but no output results from a set-measure-function event.

This event sets the default measure function to name. Subsequently, if a recursively defined function is submitted to defun with no explicitly given :measure argument, defun ``guesses'' the measure (name var), where name is the then current default measure function and var is the first formal found to be tested along every branch and changed in every recursive call.