/* Placeholder for splay-tree use only.  */