src/Pure/context.ML
changeset 27341 97e2ccba3b64
parent 26957 e3f04fdd994d
child 28122 3d099ce624e7
     1.1 --- a/src/Pure/context.ML	Tue Jun 24 19:43:16 2008 +0200
     1.2 +++ b/src/Pure/context.ML	Tue Jun 24 19:43:17 2008 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val pretty_thy: theory -> Pretty.T
     1.5    val string_of_thy: theory -> string
     1.6    val pprint_thy: theory -> pprint_args -> unit
     1.7 +  val pprint_thy_ref: theory_ref -> pprint_args -> unit
     1.8    val pretty_abbrev_thy: theory -> Pretty.T
     1.9    val str_of_thy: theory -> string
    1.10    val deref: theory_ref -> theory
    1.11 @@ -242,6 +243,8 @@
    1.12      else thy_ref
    1.13    end;
    1.14  
    1.15 +val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
    1.16 +
    1.17  
    1.18  (* consistency *)
    1.19