with_charset: setmp_noncritical;
authorwenzelm
Tue, 31 Jul 2007 21:19:23 +0200
changeset 24101 bdcefe679ced
parent 24100 a2f19514e156
child 24102 969d334040a8
with_charset: setmp_noncritical;
src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Jul 31 21:19:22 2007 +0200
+++ b/src/Pure/Thy/html.ML	Tue Jul 31 21:19:23 2007 +0200
@@ -305,7 +305,7 @@
 (* document *)
 
 val charset = ref "iso-8859-1";
-fun with_charset s = setmp charset s;
+fun with_charset s = setmp_noncritical charset s;
 
 fun begin_document title =
   "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \