Markup.add_mode;

--- a/src/Pure/Thy/html.ML	Tue Jul 10 16:45:05 2007 +0200
+++ b/src/Pure/Thy/html.ML	Tue Jul 10 16:45:06 2007 +0200
@@ -455,6 +455,6 @@
 (* mode output *)
 
 val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
-val _ = Pretty.add_mode htmlN Pretty.default_indent (span o #1);
+val _ = Markup.add_mode htmlN (span o #1);
 
 end;

--- a/src/Pure/Thy/latex.ML	Tue Jul 10 16:45:05 2007 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Jul 10 16:45:06 2007 +0200
@@ -176,6 +176,7 @@
   | latex_indent s _ = enclose "\\isaindent{" "}" s;
 
 val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
-val _ = Pretty.add_mode latexN latex_indent latex_markup;
+val _ = Markup.add_mode latexN latex_markup;
+val _ = Pretty.add_mode latexN latex_indent;
 
 end;