--- a/src/Pure/Isar/runtime.ML Sun Dec 20 13:06:26 2015 +0100
+++ b/src/Pure/Isar/runtime.ML Sun Dec 20 13:11:47 2015 +0100
@@ -76,6 +76,8 @@
SOME exns => maps (flatten context) exns
| NONE => [(context, identify exn)]);
+val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy;
+
in
fun exn_messages_ids e =
@@ -104,8 +106,7 @@
| ERROR "" => "Error"
| ERROR msg => msg
| Fail msg => raised exn "Fail" [msg]
- | THEORY (msg, thys) =>
- raised exn "THEORY" (msg :: map (robust Context.str_of_thy) thys)
+ | THEORY (msg, thys) => raised exn "THEORY" (msg :: map (robust print_thy) thys)
| Ast.AST (msg, asts) =>
raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
| TYPE (msg, Ts, ts) =>
--- 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