--- a/src/Pure/Thy/latex.ML Sun Nov 30 12:24:56 2014 +0100
+++ b/src/Pure/Thy/latex.ML Sun Nov 30 12:46:16 2014 +0100
@@ -132,8 +132,7 @@
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
- val source = Token.source_position_of tok;
- val ants = Antiquote.read (Input.source_explode source, Input.pos_of source);
+ val ants = Antiquote.read (Token.source_position_of tok);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else if Token.is_kind Token.Cartouche tok then