added pprint_thy_ref;

--- 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 *)
 

--- 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));