src/Pure/Thy/html.ML
changeset 32738 15bb09ca0378
parent 29606 fedb8be05f24
child 32796 2e4485b9a39f
     1.1 --- a/src/Pure/Thy/html.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -267,8 +267,8 @@
     1.4  
     1.5  (* document *)
     1.6  
     1.7 -val charset = ref "ISO-8859-1";
     1.8 -fun with_charset s = setmp_noncritical charset s;
     1.9 +val charset = Unsynchronized.ref "ISO-8859-1";
    1.10 +fun with_charset s = setmp_noncritical charset s;   (* FIXME *)
    1.11  
    1.12  fun begin_document title =
    1.13    let val cs = ! charset in