Makes a consequence conversion fail if applying it leaves a term unchanged.
DESCRIPTION
If c is a consequence conversion that maps a term ``t``
to a theorem |- t = t', |- t' ==> t or |- t ==> t',
where t' is alpha-equivalent to t, or if
c raises the UNCHANGED exception when applied to ``t``, then
CHANGED_CONSEQ_CONV c fails when applied to the term
``t``. Otherwise, CHANGED_CONSEQ_CONV c behaves like c.