1.1 --- a/src/Pure/context.ML	Sun Mar 18 12:51:44 2012 +0100
     1.2 +++ b/src/Pure/context.ML	Sun Mar 18 13:04:22 2012 +0100
     1.3 @@ -76,6 +76,7 @@
     1.4    (*pretty printing context*)
     1.5    val pretty: Proof.context -> pretty
     1.6    val pretty_global: theory -> pretty
     1.7 +  val pretty_generic: generic -> pretty
     1.8    val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
     1.9    (*thread data*)
    1.10    val thread_data: unit -> generic option
    1.11 @@ -557,8 +558,9 @@
    1.12  
    1.13  exception PRETTY of generic;
    1.14  
    1.15 -val pretty = Pretty o PRETTY o Proof;
    1.16 -val pretty_global = Pretty o PRETTY o Theory;
    1.17 +val pretty_generic = Pretty o PRETTY;
    1.18 +val pretty = pretty_generic o Proof;
    1.19 +val pretty_global = pretty_generic o Theory;
    1.20  
    1.21  fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
    1.22