# HG changeset patch
# User wenzelm
# Date 1211115883 -7200
# Node ID a9a1ebfb4d23bfe7afc1ab52e7d1f8fe1f11fda0
# Parent  efe3e0e235d63150546efca62f01c5ae06d86c18
pprint: proper global context via Syntax.init_pretty_global;

diff -r efe3e0e235d6 -r a9a1ebfb4d23 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sun May 18 15:04:41 2008 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sun May 18 15:04:43 2008 +0200
@@ -41,7 +41,7 @@
     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
   else Pretty.str "<context>");
 
-fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
+fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
 
 val pprint_typ = pprint Syntax.pretty_typ;
 val pprint_term = pprint Syntax.pretty_term;