# HG changeset patch # User wenzelm # Date 1222716399 -7200 # Node ID 0608c04858c74d31e4a11ef08ff6c009a4e72166 # Parent 93ec7fa3b3a0705c9d129b066b43b6c74fbe66cb back to plain Position.report for regular references; diff -r 93ec7fa3b3a0 -r 0608c04858c7 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Mon Sep 29 21:26:36 2008 +0200 +++ b/src/Pure/ML/ml_context.ML Mon Sep 29 21:26:39 2008 +0200 @@ -173,7 +173,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup (! global_parsers) name of NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME scan => (ContextPosition.report ctxt (Markup.ML_antiq name) pos; + | SOME scan => (Position.report (Markup.ML_antiq name) pos; Args.context_syntax "ML antiquotation" (scan pos) src ctxt)) end;