# HG changeset patch
# User wenzelm
# Date 1526476698 -7200
# Node ID 796f2585c7ee48cc25b78087073276c5fd752aaf
# Parent  14dd78f036bad7af49ccaa011ad5890c2faa22db
tuned;

diff -r 14dd78f036ba -r 796f2585c7ee src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed May 16 15:18:12 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed May 16 15:18:18 2018 +0200
@@ -117,13 +117,14 @@
       |> maps output_symbols_antiq
   | (SOME comment, _) => output_comment ctxt (comment, syms));
 
-in
-
 fun output_body ctxt antiq bg en syms =
   Comment.read_body syms
   |> maps (output_comment_symbols ctxt {antiq = antiq})
-  |> Latex.enclose_body bg en
-and output_token ctxt tok =
+  |> Latex.enclose_body bg en;
+
+in
+
+fun output_token ctxt tok =
   let
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));