RATOR_CONV : conv -> conv

SYNOPSIS
Applies a conversion to the operator of an application.

DESCRIPTION
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 operator of the application `t1 t2`.

FAILURE CONDITIONS
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 `(\x y. x + y) 1 2`;;
  val it : thm = |- (\x y. x + y) 1 2 = (\y. 1 + y) 2

SEE ALSO
ABS_CONV, COMB_CONV, COMB2_CONV, RAND_CONV, SUB_CONV.