--- a/LamEx.thy	Sun Dec 06 06:39:32 2009 +0100
+++ b/LamEx.thy	Sun Dec 06 06:41:52 2009 +0100
@@ -80,6 +80,35 @@
 where
   "fv \<equiv> rfv"
 
+ML {*
+local
+   fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
+   fun pp_list xs = Pretty.list "[" "]" xs
+   fun pp_str s   = Pretty.str s
+   fun pp_qstr s = Pretty.quote (pp_str s)
+   fun pp_int i   = pp_str (string_of_int i)
+   fun pp_sort S = pp_list (map pp_qstr S)
+   fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
+in
+fun raw_pp_typ (TVar ((a, i), S)) =
+       pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
+   | raw_pp_typ (TFree (a, S)) =
+       pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
+   | raw_pp_typ (Type (a, tys)) =
+       pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
+end *}
+
+ML {*
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)
+
+*}
+
+typ "name set" 
+typ "name => bool"
+
+ML {* @{typ "name set"} *}
+
 thm fv_def
 
 (* definition of overloaded permutation function *)