diff -r efc9ec539224 -r 34522db6b85a src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Sat Jan 13 12:19:03 2018 +0100 +++ b/src/Pure/Thy/latex.scala Sat Jan 13 12:51:03 2018 +0100 @@ -145,6 +145,10 @@ rest1 match { case More_Error(msg2) :: rest2 => filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) + case msg2 :: rest2 + if msg1.startsWith("Undefined control sequence") && + msg2.startsWith("\\") && msg2.containsSlice("->") => + filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) case _ => filter(rest1, (msg1, pos) :: result) }