diff -r 01aa36932739 -r f652333bbf8e src/Tools/WWW_Find/html_unicode.ML
--- a/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 18:10:37 2010 +0200
@@ -19,7 +19,7 @@
 (* mode *)
 
 val htmlunicodeN = "HTMLUnicode";
-fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
+fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
 
 (* symbol output *)