--- 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 *)