src/Pure/Syntax/lexicon.ML
changeset 39507 839873937ddd
parent 39168 e3ac771235f7
child 39510 d9f5f01faa1b
--- a/src/Pure/Syntax/lexicon.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri Sep 17 20:18:27 2010 +0200
@@ -187,11 +187,11 @@
   | EOF         => Markup.empty;
 
 fun report_token ctxt (Token (kind, _, (pos, _))) =
-  Context_Position.report ctxt (token_kind_markup kind) pos;
+  Context_Position.report ctxt pos (token_kind_markup kind);
 
 fun report_token_range ctxt tok =
   if is_proper tok
-  then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
+  then Context_Position.report ctxt (pos_of_token tok) Markup.token_range
   else ();