src/Pure/Isar/proof_display.ML
changeset 20235 3cbf73ed92f8
parent 20211 c7f907f41f7c
child 20253 636ac45d100f
     1.1 --- a/src/Pure/Isar/proof_display.ML	Thu Jul 27 13:43:12 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Jul 27 13:43:13 2006 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  structure ProofDisplay: PROOF_DISPLAY =
     1.5  struct
     1.6  
     1.7 -(* ML toplevel pretty printing *)
     1.8 +(* toplevel pretty printing *)
     1.9  
    1.10  val debug = ref false;
    1.11  
    1.12 @@ -47,7 +47,7 @@
    1.13  val pprint_term = pprint ProofContext.pretty_term;
    1.14  fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.15  fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.16 -fun pprint_thm th = pprint ProofContext.pretty_thm (Thm.theory_of_thm th) th;
    1.17 +val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
    1.18  
    1.19  
    1.20  (* theorems and theory *)