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)