strip_fun : hol_type -> hol_type list * hol_type
strip_fun(list_mk_fun([ty1,...,tyn],ty))
- strip_fun (Type `:(a -> 'bool) -> ('b -> 'c)`); > val it = ([`:a -> 'bool`, `:'b`], `:'c`) : hol_type list * hol_type