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