src/Tools/WWW_Find/html_unicode.ML
changeset 37146 f652333bbf8e
parent 33817 f6a4da31f2f1
child 37744 3daaf23b9ab4
     1.1 --- a/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  (* mode *)
     1.5  
     1.6  val htmlunicodeN = "HTMLUnicode";
     1.7 -fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
     1.8 +fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
     1.9  
    1.10  (* symbol output *)
    1.11