tuned ML message;

--- 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 *)