# HG changeset patch
# User wenzelm
# Date 975696288 -3600
# Node ID 1751ab88128938f2011b2aeded44ac2d5051fd09
# Parent  b070825579b8573b3013b29743e9fe3cc4f518c9
append print modes;

diff -r b070825579b8 -r 1751ab881289 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Fri Dec 01 19:44:15 2000 +0100
+++ b/src/Pure/Thy/html.ML	Fri Dec 01 19:44:48 2000 +0100
@@ -54,7 +54,7 @@
 (* mode *)
 
 val htmlN = "HTML";
-fun html_mode f x = setmp print_mode [htmlN] f x;
+fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;
 
 
 (* symbol output *)