rator : term -> term
STRUCTURE
Term
SYNOPSIS
Returns the operator from a combination (function application).
DESCRIPTION
If
M
is a combination, i.e., has the form
(t1 t2)
, then
rator M
returns
t1
.
FAILURE
Fails if
M
is not a combination.
SEEALSO
rand
,
dest_comb
HOL
Kananaskis-14