mk_const : string * (hol_type * hol_type) list -> term
# get_const_type "=";; val it : hol_type = `:A->A->bool` # mk_const("=",[`:num`,`:A`]);; val it : term = `(=)` # type_of it;; val it : hol_type = `:num->num->bool` # mk_const("=",[`:num`,`:A`]) = mk_mconst("=",`:num->num->bool`);; val it : bool = true