changeset 56135 | efa24d31e595 |
parent 53315 | b102e20cec78 |
--- 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;