--- a/src/Pure/Thy/latex.ML Fri Aug 15 15:50:50 2008 +0200
+++ b/src/Pure/Thy/latex.ML Fri Aug 15 15:50:52 2008 +0200
@@ -117,7 +117,7 @@
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if T.is_kind T.Verbatim tok then
let
- val (txt, pos) = T.source_of' tok;
+ val (txt, pos) = T.source_position_of tok;
val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end