--- a/src/Pure/Isar/proof_display.ML Sat Jul 29 00:51:34 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML Sat Jul 29 00:51:36 2006 +0200
@@ -47,7 +47,7 @@
val pprint_term = pprint ProofContext.pretty_term;
fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
+val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
(* theorems and theory *)