--- a/src/Pure/Thy/html.ML Fri Aug 15 17:03:55 2008 +0200
+++ b/src/Pure/Thy/html.ML Fri Aug 15 17:03:56 2008 +0200
@@ -274,7 +274,7 @@
fun begin_document title =
let val cs = ! charset in
"<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
- \<!DOCTYPE HTML PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
+ \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
\\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
\<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
\<head>\n\