src/Pure/context.ML
changeset 30628 4078276bcace
parent 29368 503ce3f8f092
child 31971 8c1b845ed105
     1.1 --- a/src/Pure/context.ML	Sat Mar 21 20:00:23 2009 +0100
     1.2 +++ b/src/Pure/context.ML	Sat Mar 21 20:00:23 2009 +0100
     1.3 @@ -27,8 +27,6 @@
     1.4    val display_names: theory -> string list
     1.5    val pretty_thy: theory -> Pretty.T
     1.6    val string_of_thy: theory -> string
     1.7 -  val pprint_thy: theory -> pprint_args -> unit
     1.8 -  val pprint_thy_ref: theory_ref -> pprint_args -> unit
     1.9    val pretty_abbrev_thy: theory -> Pretty.T
    1.10    val str_of_thy: theory -> string
    1.11    val deref: theory_ref -> theory
    1.12 @@ -228,7 +226,6 @@
    1.13  
    1.14  val pretty_thy = Pretty.str_list "{" "}" o display_names;
    1.15  val string_of_thy = Pretty.string_of o pretty_thy;
    1.16 -val pprint_thy = Pretty.pprint o pretty_thy;
    1.17  
    1.18  fun pretty_abbrev_thy thy =
    1.19    let
    1.20 @@ -256,8 +253,6 @@
    1.21      else thy_ref
    1.22    end;
    1.23  
    1.24 -val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
    1.25 -
    1.26  
    1.27  (* build ids *)
    1.28