dest_ptree : term -> term_ptree
STRUCTURE
patriciaLib
SYNOPSIS
Term destructor for Patricia trees.
DESCRIPTION
The destructor dest_ptree will return a Patricia tree in ML that corresponds with the supplied HOL term. The ML abstract data type term_ptree is defined in patriciaLib.
FAILURE
The conversion will fail if the supplied term is not well constructed Patricia tree.
EXAMPLE
- dest_ptree ``(Branch 1 2 (Leaf 2 2) (Leaf 3 3))``;
Exception-
   HOL_ERR
  {message = "not a valid Patricia tree", origin_function = "dest_ptree",
  origin_structure = "patricia"} raised

- dest_ptree ``(Branch 0 0 (Leaf 3 3) (Leaf 2 2))``;
val it = <ptree>: term_ptree
COMMENTS
By default PolyML prints abstract data types in full. This can be turned off with: 
let
  fun pp _ _ (_: term_ptree) = PolyML.PrettyString "<ptree>"
in
  PolyML.addPrettyPrinter pp
end;
SEEALSO
mk_ptree, is_ptree
HOL  Kananaskis-13