pprint: proper global context via Syntax.init_pretty_global;
authorwenzelm
Sun, 18 May 2008 15:04:43 +0200
changeset 26949 a9a1ebfb4d23
parent 26948 efe3e0e235d6
child 26950 80366b6eb94c
pprint: proper global context via Syntax.init_pretty_global;
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;