src/Pure/Thy/html.ML
changeset 39616 8052101883c3
parent 37941 1d812ff95a14
child 40946 3f697c636fa1
--- a/src/Pure/Thy/html.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -277,7 +277,7 @@
 (* document *)
 
 val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s;   (* FIXME unreliable *)
+fun with_charset s = Unsynchronized.setmp charset s;   (* FIXME unreliable *)
 
 fun begin_document title =
   let val cs = ! charset in