diff -r 4a7a07c01857 -r efa24d31e595 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Thu Mar 13 10:34:48 2014 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Thu Mar 13 11:34:05 2014 +0100
@@ -177,7 +177,7 @@
 
 local
 val (fromsym, fromabbr, tosym, toabbr) =
-  read_symbols (Path.explode "~~/src/Tools/WWW_Find/etc/symbols");
+  read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
 in
 val symbol_to_unicode = Symtab.lookup fromsym;
 val abbrev_to_unicode = Symtab.lookup fromabbr;