changeset 10573 | 1751ab881289 |
parent 9963 | 6342d9c7fe46 |
child 10831 | 024bdf8e52a4 |
--- 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 *)