----------------------------------------------------------------------
apply                                                          (Count)
----------------------------------------------------------------------
apply : ('a -> 'b) -> 'a -> 'b

SYNOPSIS
Counts primitive inferences performed when a function is applied.

KEYWORDS


DESCRIBE
The {apply} function provides a way of counting the primitive
inferences that are performed when a function is applied to its
argument.  The reporting of the count is done when the function
terminates (normally, or with an exception).  The reporting also
includes timing information about the function call.

EXAMPLE

- Count.apply (CONJUNCTS o SPEC_ALL) AND_CLAUSES;
runtime: 0.000s,    gctime: 0.000s,     systime: 0.000s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 9; Total: 9
val it =
   [|- T /\ t <=> t,
    |- t /\ T <=> t, |- F /\ t <=> F,
    |- t /\ F <=> F,
    |- t /\ t <=> t]: thm list


FAILURE
The call to {apply f x} will raise an exception if {f x} would.  It
will still report elapsed time and inference counts up to the point of
the exception being raised.

SEEALSO
Count.thm_count.

----------------------------------------------------------------------