# HG changeset patch
# User wenzelm
# Date 1251893505 -7200
# Node ID 6a48db3e627ce25f5a76fe61efa1c13c2bf4719f
# Parent  071e4ae8314942caccf0f6f6285c7065d90ab00f
tuned ML message;

diff -r 071e4ae83149 -r 6a48db3e627c src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 02 12:20:17 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 02 14:11:45 2009 +0200
@@ -111,9 +111,8 @@
     fun put s = change output_buffer (Buffer.add s);
 
     fun put_message {message, hard, location, context = _} =
-     (put (if hard then "Error: " else "Warning: ");
-      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
-      put (Position.str_of (position_of location) ^ "\n"));
+     (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
+      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)) ^ "\n"));
 
 
     (* results *)