ABS_CONV : conv -> conv

SYNOPSIS
Applies a conversion to the body of an abstraction.

DESCRIPTION
If c is a conversion that maps a term `t` to the theorem |- t = t', then the conversion ABS_CONV c maps abstractions of the form `\x. t` to theorems of the form:
   |- (\x. t) = (\x. t')
That is, ABS_CONV c `\x. t` applies c to the body of the abstraction `\x. t`.

FAILURE CONDITIONS
ABS_CONV c tm fails if tm is not an abstraction or if tm has the form `\x. t` but the conversion c fails when applied to the term t, or if the theorem returned has assumptions in which the abstracted variable x is free. The function returned by ABS_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
  # ABS_CONV SYM_CONV `\x. 1 = x`;;
  val it : thm = |- (\x. 1 = x) = (\x. x = 1)

SEE ALSO
GABS_CONV, RAND_CONV, RATOR_CONV, SUB_CONV.