diff -r 86aa6e2abee1 -r 820f3cbae27a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Jan 08 11:41:16 2018 +0100
@@ -273,11 +273,14 @@
     Scan.option (Symbol_Pos.scan_cartouche_content "Document token error: ")
       >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
 
+val read_symbols_comment =
+  Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment);
+
 in
 
 fun output_body state antiq bg en syms =
   (if exists (fn (s, _) => s = Symbol.comment) syms then
-    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms of
+    (case read_symbols_comment syms of
       SOME res => maps (output_symbols_comment state {antiq = antiq}) res
     | NONE => output_symbols syms)
    else output_symbols syms) |> Latex.enclose_body bg en