src/Pure/library.scala

--- a/src/Pure/library.scala	Wed Nov 20 23:14:06 2013 +0100
+++ b/src/Pure/library.scala	Thu Nov 21 17:45:37 2013 +0100
@@ -26,9 +26,12 @@
 
   def error(message: String): Nothing = throw ERROR(message)
 
+  def cat_message(msg1: String, msg2: String): String =
+    if (msg1 == "") msg2
+    else msg1 + "\n" + msg2
+
   def cat_error(msg1: String, msg2: String): Nothing =
-    if (msg1 == "") error(msg1)
-    else error(msg1 + "\n" + msg2)
+    error(cat_message(msg1, msg2))
 
 
   /* separated chunks */