--- a/src/Pure/context.ML Sun Dec 20 13:06:26 2015 +0100
+++ b/src/Pure/context.ML Sun Dec 20 13:11:47 2015 +0100
@@ -37,9 +37,7 @@
val theory_name: theory -> string
val PureN: string
val pretty_thy: theory -> Pretty.T
- val string_of_thy: theory -> string
val pretty_abbrev_thy: theory -> Pretty.T
- val str_of_thy: theory -> string
val get_theory: theory -> string -> theory
val this_theory: theory -> string -> theory
val eq_thy_id: theory_id * theory_id -> bool
@@ -170,7 +168,6 @@
in rev (name :: ancestor_names) end;
val pretty_thy = Pretty.str_list "{" "}" o display_names;
-val string_of_thy = Pretty.string_of o pretty_thy;
fun pretty_abbrev_thy thy =
let
@@ -179,8 +176,6 @@
val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
in Pretty.str_list "{" "}" abbrev end;
-val str_of_thy = Pretty.unformatted_string_of o pretty_abbrev_thy;
-
fun get_theory thy name =
if theory_name thy <> name then
(case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of