diff -r 27246f8b2dac -r 890e983cb07b src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Mon Nov 11 18:37:56 2013 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Mon Nov 11 20:00:53 2013 +0100
@@ -9,6 +9,7 @@
   val exn_messages_ids: exn -> Runtime.error list
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
+  val exn_error_message: exn -> unit
   val exn_trace: (unit -> 'a) -> 'a
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
@@ -23,6 +24,8 @@
 val exn_messages_ids = Runtime.exn_messages_ids exn_info;
 val exn_messages = Runtime.exn_messages exn_info;
 val exn_message = Runtime.exn_message exn_info;
+
+val exn_error_message = Output.error_message o exn_message;
 fun exn_trace e = print_exception_trace exn_message e;
 
 fun eval verbose pos toks =