Applies a conversion to the operand of an application.
DESCRIPTION
If c is a conversion that maps a term `t2` to the theorem |- t2 = t2',
then the conversion RAND_CONV c maps applications of the form `t1 t2` to
theorems of the form:
|- (t1 t2) = (t1 t2')
That is, RAND_CONV c `t1 t2` applies c to the operand of the
application `t1 t2`.
FAILURE CONDITIONS
RAND_CONV c tm fails if tm is not an application or if tm has the form
`t1 t2` but the conversion c fails when applied to the term t2. The
function returned by RAND_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').
EXAMPLE
# RAND_CONV num_CONV `SUC 2`;;
val it : thm = |- SUC 2 = SUC (SUC 1)