replaced Hol_datatype with Datatype
BVL/BVP now use sptrees instead of finite maps