src/Pure/Isar/runtime.ML

   | flatten context exn =
       (case Par_Exn.dest exn of
         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 =
   let
     fun raised exn name msgs =

               TimeLimit.TimeOut => "Timeout"
             | TOPLEVEL_ERROR => "Error"
             | 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) =>
                 raised exn "TYPE" (msg ::
                   (robust_context context Syntax.string_of_typ Ts @