# HG changeset patch
# User wenzelm
# Date 1266522262 -3600
# Node ID 2e37cdae7b9ca8434aea29d2ce49da5312f7e058
# Parent  f95c6440c1c7af45d9c384c7dd6b7811de670306
pretty_full_theory: proper Syntax.init_pretty_global;

diff -r f95c6440c1c7 -r 2e37cdae7b9c src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Feb 18 11:23:03 2010 +0100
+++ b/src/Pure/display.ML	Thu Feb 18 20:44:22 2010 +0100
@@ -125,7 +125,7 @@
 
 fun pretty_full_theory verbose thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = Syntax.init_pretty_global thy;
 
     fun prt_cls c = Syntax.pretty_sort ctxt [c];
     fun prt_sort S = Syntax.pretty_sort ctxt S;