src/Pure/display.ML
changeset 10737 c130eb1e863f
parent 10010 f6ccb6df9cb9
child 11501 3b6415035d1a
     1.1 --- a/src/Pure/display.ML	Sat Dec 23 22:52:18 2000 +0100
     1.2 +++ b/src/Pure/display.ML	Sat Dec 23 22:52:41 2000 +0100
     1.3 @@ -163,7 +163,7 @@
     1.4      fun prt_cls c = Sign.pretty_sort sg [c];
     1.5      fun prt_sort S = Sign.pretty_sort sg S;
     1.6      fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
     1.7 -    fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
     1.8 +    fun prt_typ_no_tvars ty = Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)));
     1.9      fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
    1.10  
    1.11      fun pretty_classes cs = Pretty.block
    1.12 @@ -184,17 +184,17 @@
    1.13  
    1.14      fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
    1.15        | pretty_witness (Some (T, S)) = Pretty.block
    1.16 -          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ T,
    1.17 +          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ_no_tvars T,
    1.18              Pretty.brk 1, prt_sort S];
    1.19  
    1.20      fun pretty_abbr (t, (vs, rhs)) = Pretty.block
    1.21 -      [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.22 -        Pretty.str " =", Pretty.brk 1, prt_typ rhs];
    1.23 +      [prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.24 +        Pretty.str " =", Pretty.brk 1, prt_typ_no_tvars rhs];
    1.25  
    1.26      fun pretty_arities (t, ars) = map (prt_arity t) ars;
    1.27  
    1.28      fun pretty_const (c, ty) = Pretty.block
    1.29 -      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
    1.30 +      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.31  
    1.32      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    1.33