author | wenzelm |
Fri Dec 01 19:44:48 2000 +0100 (2000-12-01) | |
changeset 10573 | 1751ab881289 |
parent 10572 | b070825579b8 |
child 10574 | 8f98f0301d67 |
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 *)