src/Pure/library.scala

--- a/src/Pure/library.scala	Sat Mar 14 20:08:03 2015 +0100
+++ b/src/Pure/library.scala	Sat Mar 14 20:49:10 2015 +0100
@@ -16,9 +16,21 @@
 {
   /* user errors */
 
+  class User_Error(message: String) extends RuntimeException(message)
+  {
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: User_Error => message == other.getMessage
+        case _ => false
+      }
+    override def hashCode: Int = message.hashCode
+
+    override def toString: String = "ERROR(" + message + ")"
+  }
+
   object ERROR
   {
-    def apply(message: String): Throwable = new RuntimeException(message)
+    def apply(message: String): User_Error = new User_Error(message)
     def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
   }