ensure separation of TeX tokens;

--- a/src/Pure/Thy/latex.ML	Tue Dec 12 16:12:48 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Dec 12 17:47:00 2017 +0100
@@ -189,7 +189,7 @@
       (case take_prefix is_blank_line (split_lines output) of
         (_, []) => output
       | (blank, rest) =>
-          cat_lines blank ^ "%\n" ^
+          cat_lines blank ^ " %\n" ^
           output_prop (Markup.lineN, Value.print_int n) ^
           cat_lines rest));