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