Attempts to apply a conversion; applies identity conversion in case of failure.
DESCRIPTION
TRY_CONV c `t` attempts to apply the conversion c to the term `t`; if
this fails, then the identity conversion is applied instead giving the
reflexive theorem |- t = t.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# num_CONV `0`;;
Exception: Failure "num_CONV".
# TRY_CONV num_CONV `0`;;
val it : thm = |- 0 = 0