# HG changeset patch
# User wenzelm
# Date 1450613507 -3600
# Node ID fa4dbb82732fc28f869bd0889702e83e39ee033e
# Parent  276ad43540693a4c278876c89cfd9eeee6a8cd3a
tuned signature;

diff -r 276ad4354069 -r fa4dbb82732f src/Pure/Isar/runtime.ML
--- 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) =>
diff -r 276ad4354069 -r fa4dbb82732f src/Pure/context.ML
--- 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