more basic ML compiler messages -- avoid conflict of 638cefe3ee99 and cb7264721c91 concerning Protocol.message_positions;

--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Oct 11 23:10:49 2012 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Oct 12 11:03:23 2012 +0200
@@ -113,10 +113,8 @@
       let
         val pos = position_of loc;
         val txt =
-          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
-            ((if hard then "Error" else "Warning") ^ Position.here pos ^ ":\n") ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Position.reported_text pos Isabelle_Markup.report "";
+          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
+          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
       in if hard then err txt else warn txt end;