# HG changeset patch
# User wenzelm
# Date 911307892 -3600
# Node ID c39b23d752b6fe54c38c713afa87b540b88310a9
# Parent  a8e1ca1b2ec6a760701e96c12c1fa1657f36a7b9
Pretty.spc;

diff -r a8e1ca1b2ec6 -r c39b23d752b6 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Nov 17 14:04:32 1998 +0100
+++ b/src/Pure/display.ML	Tue Nov 17 14:04:52 1998 +0100
@@ -146,7 +146,7 @@
       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
 
     fun pretty_ty (t, n) = Pretty.block
-      [Pretty.str (ext_tycon t), Pretty.str (" " ^ string_of_int n)];
+      [Pretty.str (ext_tycon t), Pretty.spc 1, Pretty.str (string_of_int n)];
 
     fun pretty_abbr (t, (vs, rhs)) = Pretty.block
       [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),