----------------------------------------------------------------------
dest_strip_comb                                           (boolSyntax)
----------------------------------------------------------------------
dest_strip_comb : term -> string * term list

SYNOPSIS
Strips a function application, and breaks head constant.

KEYWORDS


DESCRIBE
If {t} is a term of the form {c t1 t2 .. tn}, with {c} a constant,
then a call to {dest_strip_comb t} returns a pair {(s,[t1,...,tn])},
where {s} is a string of the form {thy$name}. The {thy} prefix
identifies the theory where the constant was defined, and the {name}
suffix is the constant’s name.

FAILURE
Fails if the term is not a constant applied to zero or more arguments.

EXAMPLE

> dest_strip_comb ``SUC 2``;
val it = ("num$SUC", [``2``]) : string * term list


COMMENTS
Useful for pattern-matching at the ML level, where doing a {case} on
{Lib.total dest_strip_comb t} allows patterns of interest to be
idiomatically identified. In the absence of view-patterns in SML, one
has to use custom destructors.

SEEALSO
HolKernel.dest_term.

----------------------------------------------------------------------