----------------------------------------------------------------------
disch                                                      (HolKernel)
----------------------------------------------------------------------
disch : ((term * term list) -> term list)

SYNOPSIS
Removes those elements of a list of terms that are alpha equivalent to a
given term.

DESCRIBE
Given a pair {(t,tl)} of term {t} and term list {tl}, {disch} removes
those elements of {tl} that are  alpha equivalent to {t}.

EXAMPLE

> disch (``\x:bool.T``, [``A = T``, ``B = 3``, ``\y:bool.T``]);
val it = [``A = T``,``B = 3``] : term list




SEEALSO
Lib.filter.

----------------------------------------------------------------------