diff -r 20aea331137f -r 992c6d984925 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Mon Aug 11 22:06:49 2008 +0200
+++ b/src/Pure/Thy/html.ML	Mon Aug 11 22:06:51 2008 +0200
@@ -333,8 +333,8 @@
           "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
           \<applet code=\"GraphBrowser/GraphBrowser.class\" \
           \archive=\"GraphBrowser.jar\" \
-          \width=" ^ width ^ " height=" ^ height ^ ">\n\
-          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
+          \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
+          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
           \</applet>\n<hr/>" ^ end_document)
       end;
   in map applet_page sizes end;