src/Pure/display.ML
changeset 35845 e5980f0ad025
parent 35199 2e37cdae7b9c
child 36328 4d9deabf6474
     1.1 --- a/src/Pure/display.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Pure/display.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -131,9 +131,9 @@
     1.4      fun prt_sort S = Syntax.pretty_sort ctxt S;
     1.5      fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
     1.6      fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
     1.7 -    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
     1.8 +    val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
     1.9      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
    1.10 -    val prt_term_no_vars = prt_term o Logic.unvarify;
    1.11 +    val prt_term_no_vars = prt_term o Logic.unvarify_global;
    1.12      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.13      val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
    1.14