src/Pure/display.ML
changeset 5902 c39b23d752b6
parent 5245 a6167c446b0b
child 6087 c8ec08fced15
equal deleted inserted replaced
5901:a8e1ca1b2ec6 5902:c39b23d752b6
   144 
   144 
   145     fun pretty_default S = Pretty.block
   145     fun pretty_default S = Pretty.block
   146       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
   146       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
   147 
   147 
   148     fun pretty_ty (t, n) = Pretty.block
   148     fun pretty_ty (t, n) = Pretty.block
   149       [Pretty.str (ext_tycon t), Pretty.str (" " ^ string_of_int n)];
   149       [Pretty.str (ext_tycon t), Pretty.spc 1, Pretty.str (string_of_int n)];
   150 
   150 
   151     fun pretty_abbr (t, (vs, rhs)) = Pretty.block
   151     fun pretty_abbr (t, (vs, rhs)) = Pretty.block
   152       [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   152       [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   153         Pretty.str " =", Pretty.brk 1, prt_typ rhs];
   153         Pretty.str " =", Pretty.brk 1, prt_typ rhs];
   154 
   154