bvar : term -> term
STRUCTURE
SYNOPSIS
Returns the bound variable of an abstraction.
DESCRIPTION
If M is a lambda abstraction, i.e, has the form \v. t, then bvar M returns v.
FAILURE
Fails unless M is an abstraction.
SEEALSO
HOL  Trindemossen-1