src/Pure/Thy/latex.ML
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30642 0c9f9c49d5df
     1.1 --- a/src/Pure/Thy/latex.ML	Fri Mar 20 20:20:09 2009 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Fri Mar 20 20:21:38 2009 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4      else if T.is_kind T.Verbatim tok then
     1.5        let
     1.6          val (txt, pos) = T.source_position_of tok;
     1.7 -        val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     1.8 +        val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     1.9          val out = implode (map output_syms_antiq ants);
    1.10        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    1.11      else output_syms s