diff -r a21d3e1e64fd -r fe6d1ae7a065 src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/Pure/System/invoke_scala.scala	Fri Aug 12 11:41:26 2011 +0200
@@ -57,10 +57,8 @@
         Exn.capture { f(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
-          case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
-          case Exn.Exn(e) => (Tag.ERROR, e.toString)
+          case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
-      case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
-      case Exn.Exn(e) => (Tag.FAIL, e.toString)
+      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
     }
 }