src/Pure/Isar/proof_display.ML
changeset 24920 2a45e400fdad
parent 22872 d7189dc8939c
child 26336 a0e2b706ce73
     1.1 --- a/src/Pure/Isar/proof_display.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -43,8 +43,8 @@
     1.4  
     1.5  fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
     1.6  
     1.7 -val pprint_typ = pprint ProofContext.pretty_typ;
     1.8 -val pprint_term = pprint ProofContext.pretty_term;
     1.9 +val pprint_typ = pprint Syntax.pretty_typ;
    1.10 +val pprint_term = pprint Syntax.pretty_term;
    1.11  fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.12  fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.13  val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
    1.14 @@ -136,7 +136,7 @@
    1.15  
    1.16  fun pretty_var ctxt (x, T) =
    1.17    Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
    1.18 -    Pretty.quote (ProofContext.pretty_typ ctxt T)];
    1.19 +    Pretty.quote (Syntax.pretty_typ ctxt T)];
    1.20  
    1.21  fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
    1.22