----------------------------------------------------------------------
RATOR_CONV                                                      (Conv)
----------------------------------------------------------------------
RATOR_CONV : (conv -> conv)

SYNOPSIS
Applies a conversion to the operator of an application.

KEYWORDS
conversional.

DESCRIBE
If {c} is a conversion that maps a term {"t1"} to the theorem {|- t1 = t1'},
then the conversion {RATOR_CONV c} maps applications of the form {"t1 t2"} to
theorems of the form:

   |- (t1 t2) = (t1' t2)

That is, {RATOR_CONV c "t1 t2"} applies {c} to the operand of the
application {"t1 t2"}.

FAILURE
{RATOR_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 {t1}. The
function returned by {RATOR_CONV c} may also fail if the ML function
{c:term->thm} is not, in fact, a conversion (i.e. a function that maps a term
{t} to a theorem {|- t = t'}).

EXAMPLE

- RATOR_CONV BETA_CONV (Term `(\x y. x + y) 1 2`);
> val it = |- (\x y. x + y)1 2 = (\y. 1 + y) 2 : thm




SEEALSO
Conv.ABS_CONV, Conv.RAND_CONV, Conv.SUB_CONV.

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