mk_ptree : term_ptree -> term
STRUCTURE
patriciaLib
SYNOPSIS
Term constructor for Patricia trees.
DESCRIPTION
The constructor mk_ptree will return a HOL term that corresponds with the supplied ML Patricia tree. The ML abstract data type term_ptree is defined in patriciaLib.
FAILURE
The conversion will fail if the terms stored in the supplied Patricia tree do not all have the same type.
EXAMPLE
- mk_ptree (int_ptree_of_list [(1,``T``), (2, ``2``)]);
Exception-
   HOL_ERR
  {message = "", origin_function = "mk_branch", origin_structure =
  "HolKernel"} raised

- mk_ptree (int_ptree_of_list [(1,``1``), (2, ``2``)]);
val it = ``Branch 0 0 (Leaf 1 1) (Leaf 2 2)``: term
COMMENTS
When working with large trees it is a good idea constrain term printing by setting Globals.max_print_depth.
SEEALSO
dest_ptree, is_ptree
HOL  Trindemossen-1