dest_arb : term -> hol_type
STRUCTURE
SYNOPSIS
Extract the type of an instance of the ARB constant.
LIBRARY
DESCRIPTION
If M is an instance of the constant ARB with type ty, then dest_arb M equals ty.
FAILURE
Fails if M is not an instance of ARB.
COMMENTS
When it succeeds, an invocation of dest_arb is equivalent to type_of.
SEEALSO
HOL  Kananaskis-13