--- a/src/Pure/Syntax/lexicon.ML Sun Aug 08 19:36:31 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML Sun Aug 08 19:54:54 2010 +0200
@@ -65,7 +65,7 @@
val tvarT: typ
val terminals: string list
val is_terminal: string -> bool
- val report_token: token -> unit
+ val report_token: Proof.context -> token -> unit
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
@@ -185,8 +185,8 @@
| Comment => Markup.inner_comment
| EOF => Markup.none;
-fun report_token (Token (kind, _, (pos, _))) =
- Position.report (token_kind_markup kind) pos;
+fun report_token ctxt (Token (kind, _, (pos, _))) =
+ Context_Position.report ctxt (token_kind_markup kind) pos;
(* matching_tokens *)