append print modes;
authorwenzelm
Fri Dec 01 19:44:48 2000 +0100 (2000-12-01)
changeset 105731751ab881289
parent 10572 b070825579b8
child 10574 8f98f0301d67
append print modes;
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Thy/html.ML	Fri Dec 01 19:44:15 2000 +0100
     1.2 +++ b/src/Pure/Thy/html.ML	Fri Dec 01 19:44:48 2000 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  (* mode *)
     1.5  
     1.6  val htmlN = "HTML";
     1.7 -fun html_mode f x = setmp print_mode [htmlN] f x;
     1.8 +fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;
     1.9  
    1.10  
    1.11  (* symbol output *)