src/Pure/display.ML
changeset 19806 f860b7a98445
parent 19703 9c84266e1d5f
child 20076 def4ad161528
     1.1 --- a/src/Pure/display.ML	Wed Jun 07 02:01:27 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Jun 07 02:01:28 2006 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4      fun prt_sort S = Sign.pretty_sort thy S;
     1.5      fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
     1.6      fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
     1.7 -    val prt_typ_no_tvars = prt_typ o Type.freeze_type;
     1.8 +    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
     1.9      fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
    1.10      val prt_term_no_vars = prt_term o Logic.unvarify;
    1.11      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];