src/Pure/context.ML
changeset 30628 4078276bcace
parent 29368 503ce3f8f092
child 31971 8c1b845ed105
--- a/src/Pure/context.ML	Sat Mar 21 20:00:23 2009 +0100
+++ b/src/Pure/context.ML	Sat Mar 21 20:00:23 2009 +0100
@@ -27,8 +27,6 @@
   val display_names: 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
@@ -228,7 +226,6 @@
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 val string_of_thy = Pretty.string_of o pretty_thy;
-val pprint_thy = Pretty.pprint o pretty_thy;
 
 fun pretty_abbrev_thy thy =
   let
@@ -256,8 +253,6 @@
     else thy_ref
   end;
 
-val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
-
 
 (* build ids *)