src/Pure/context.ML

   val exists_name: string -> theory -> bool
   val names_of: theory -> string list
   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
   val check_thy: theory -> theory_ref
   val eq_thy: theory * theory -> bool

   let val thy_ref = TheoryRef (the_self thy) in
     if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
     else thy_ref
   end;
 
+val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
+
 
 (* consistency *)
 
 fun check_ins id ids =
   if draft_id id orelse Inttab.defined ids (#1 id) then ids