 SYNOPSIS

Applies a conversion to the toplevel subterms of a term.
 DESCRIPTION

For any conversion c, the function returned by SUB_CONV c is a conversion
that applies c to all the toplevel subterms of a term. If the conversion
c maps t to  t = t', then SUB_CONV c maps an abstraction `\x. t` to
the theorem:
That is, SUB_CONV c `\x. t` applies c to the body of the
abstraction `\x. t`. If c is a conversion that maps `t1` to the theorem
 t1 = t1' and `t2` to the theorem  t2 = t2', then the conversion
SUB_CONV c maps an application `t1 t2` to the theorem:
That is, SUB_CONV c `t1 t2` applies c to the both the operator
t1 and the operand t2 of the application `t1 t2`. Finally, for any
conversion c, the function returned by SUB_CONV c acts as the identity
conversion on variables and constants. That is, if `t` is a variable or
constant, then SUB_CONV c `t` returns  t = t.
 FAILURE CONDITIONS

SUB_CONV c tm fails if tm is an abstraction `\x. t` and the conversion c
fails when applied to t, or if tm is an application `t1 t2` and the
conversion c fails when applied to either t1 or t2. The function
returned by SUB_CONV c may also fail if the ML function c is not, in fact,
a conversion (i.e. a function that maps a term t to a theorem  t = t').
 SEE ALSO

ABS_CONV, COMB_CONV, RAND_CONV, RATOR_CONV.