Parse.type_abbrev_pp : string * hol_type -> unit
> type_abbrev_pp ("foo", ``:num -> 'a # num``); val it = () : unit > ``:bool foo``; val it = ``:bool foo``: hol_type > dest_thy_type it; val it = {Args = [``:num``, ``:bool # num``], Thy = "min", Tyop = "fun"}: {Args: hol_type list, Thy: string, Tyop: string}