83 ML {*

    84 local

    85    fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]

    86    fun pp_list xs = Pretty.list "[" "]" xs

    87    fun pp_str s   = Pretty.str s

    88    fun pp_qstr s = Pretty.quote (pp_str s)

    89    fun pp_int i   = pp_str (string_of_int i)

    90    fun pp_sort S = pp_list (map pp_qstr S)

    91    fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]

    92 in

    93 fun raw_pp_typ (TVar ((a, i), S)) =

    94        pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))

    95    | raw_pp_typ (TFree (a, S)) =

    96        pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))

    97    | raw_pp_typ (Type (a, tys)) =

    98        pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))

    99 end *}

   100 

   101 ML {*

   102 PolyML.addPrettyPrinter

   103   (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)

   104 

   105 *}

   106 

   107 typ "name set" 

   108 typ "name => bool"

   109 

   110 ML {* @{typ "name set"} *}

   111