| changeset 23935 | 2a4e42ec9a54 |
| parent 23724 | 6e95ed5f64da |
| child 24101 | bdcefe679ced |
--- a/src/Pure/Thy/html.ML Mon Jul 23 16:45:02 2007 +0200 +++ b/src/Pure/Thy/html.ML Mon Jul 23 16:45:03 2007 +0200 @@ -51,7 +51,7 @@ (* mode *) val htmlN = "HTML"; -fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x; +fun html_mode f x = PrintMode.with_modes [htmlN] f x; (* symbol output *)