1\DOC 2 3\TYPE {dest_strip_comb : term -> string * term list} 4 5\SYNOPSIS 6Strips a function application, and breaks head constant. 7 8\KEYWORDS 9 10\DESCRIBE 11If {t} is a term of the form {c t1 t2 .. tn}, with {c} a constant, 12then a call to {dest_strip_comb t} returns a pair {(s,[t1,...,tn])}, 13where {s} is a string of the form {thy$name}. The {thy} prefix 14identifies the theory where the constant was defined, and the {name} 15suffix is the constant���s name. 16 17\FAILURE 18Fails if the term is not a constant applied to zero or more arguments. 19 20\EXAMPLE 21{ 22> dest_strip_comb ``SUC 2``; 23val it = ("num$SUC", [``2``]) : string * term list 24} 25 26\COMMENTS 27Useful for pattern-matching at the ML level, where doing a {case} on 28{Lib.total dest_strip_comb t} allows patterns of interest to be 29idiomatically identified. In the absence of view-patterns in SML, one 30has to use custom destructors. 31 32\SEEALSO 33HolKernel.dest_term. 34 35\ENDDOC 36