# HG changeset patch
# User wenzelm
# Date 1214329397 -7200
# Node ID 97e2ccba3b642038df5f119e2e67d4addf002cab
# Parent  3de9f20f4e28bd13a0c7c25ed692bdf25b63281a
added pprint_thy_ref;

diff -r 3de9f20f4e28 -r 97e2ccba3b64 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Jun 24 19:43:16 2008 +0200
+++ b/src/Pure/context.ML	Tue Jun 24 19:43:17 2008 +0200
@@ -29,6 +29,7 @@
   val pretty_thy: theory -> Pretty.T
   val string_of_thy: theory -> string
   val pprint_thy: theory -> pprint_args -> unit
+  val pprint_thy_ref: theory_ref -> pprint_args -> unit
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
   val deref: theory_ref -> theory
@@ -242,6 +243,8 @@
     else thy_ref
   end;
 
+val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
+
 
 (* consistency *)
 
diff -r 3de9f20f4e28 -r 97e2ccba3b64 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Jun 24 19:43:16 2008 +0200
+++ b/src/Pure/pure_setup.ML	Tue Jun 24 19:43:17 2008 +0200
@@ -32,6 +32,7 @@
 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
+install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
 install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
 install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));