ML_Compiler.exn_message;

--- a/src/HOL/Tools/res_reconstruct.ML	Sat Jun 06 21:11:23 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sat Jun 06 21:46:36 2009 +0200
@@ -452,7 +452,7 @@
     isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
   end
   handle e => (*FIXME: exn handler is too general!*)
-    let val msg = "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e
+    let val msg = "Translation of TSTP raised an exception: " ^ ML_Compiler.exn_message e
     in  trace msg; msg  end;