src/Pure/display.ML
changeset 24920 2a45e400fdad
parent 24848 5dbbd33c3236
child 25405 7ac8c93be624
     1.1 --- a/src/Pure/display.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -146,12 +146,14 @@
     1.4  
     1.5  fun pretty_full_theory verbose thy =
     1.6    let
     1.7 -    fun prt_cls c = Sign.pretty_sort thy [c];
     1.8 -    fun prt_sort S = Sign.pretty_sort thy S;
     1.9 -    fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
    1.10 -    fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
    1.11 +    val ctxt = ProofContext.init thy;
    1.12 +
    1.13 +    fun prt_cls c = Syntax.pretty_sort ctxt [c];
    1.14 +    fun prt_sort S = Syntax.pretty_sort ctxt S;
    1.15 +    fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
    1.16 +    fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
    1.17      val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
    1.18 -    fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
    1.19 +    fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
    1.20      val prt_term_no_vars = prt_term o Logic.unvarify;
    1.21      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.22      val prt_const' = Defs.pretty_const (Sign.pp thy);