mk_type(tyop,[ty1,...,tyn]) returns the HOL type (ty1,...,tyn)tyop,
provided tyop is the name of a known n-ary type constructor.
FAILURE
Fails if tyop is not the name of a known type, or if tyop is known,
but the length of the list of argument types is not equal to the arity
of tyop.
EXAMPLE
- mk_type ("bool",[]);
> val it = `:bool` : hol_type
- mk_type ("fun",[alpha,it]);
> val it = `:'a -> bool` : hol_type
COMMENTS
Note that type operators with the same name (and arity) may
be declared in different theories. If two theories having type
operators with the same name s are in the ancestry of the current
theory, then mk_type(s,tyl) will issue a warning before arbitrarily
selecting which type operator to use. In such situations, it is
preferable to use mk_thy_type since it allows one to specify
exactly which type operator to use.