diff -r a6e71e5a1004 -r d8c809afafb8 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue May 19 17:15:04 1998 +0200
+++ b/src/Pure/library.ML	Tue May 19 17:15:30 1998 +0200
@@ -1053,12 +1053,12 @@
 
 fun handle_error f x =
   let
-    val buffer = ref "";
-    fun capture s = buffer := ! buffer ^ s ^ "\n";
+    val buffer = ref ([]: string list);
+    fun capture s = buffer := ! buffer @ [s];
     val result = Some (setmp error_fn capture f x) handle ERROR => None;
   in
     (case result of
-      None => Error (! buffer)
+      None => Error (cat_lines (! buffer))
     | Some y => OK y)
   end;