--- a/src/Pure/ML/ml_lex.ML Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML Fri Sep 17 20:18:27 2010 +0200
@@ -112,7 +112,7 @@
in
-fun report_token (Token ((pos, _), (kind, x))) = Position.report (token_markup kind x) pos;
+fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
end;
@@ -265,7 +265,7 @@
fun read pos txt =
let
- val _ = Position.report Markup.ML_source pos;
+ val _ = Position.report pos Markup.ML_source;
val syms = Symbol_Pos.explode (txt, pos);
val termination =
if null syms then []