diff -r 4a6df182b093 -r d28dff7ac48d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Oct 13 19:40:23 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Oct 13 19:41:18 1999 +0200
@@ -64,8 +64,8 @@
         else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
         else output_sym s
       end
-  | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
-  | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n";
+  | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
+  | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
 
 
 val output_tokens = implode o map output_tok;