diff -r fd650d659275 -r 8c89a1fb30f2 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Thu Jun 30 11:15:36 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Thu Jun 30 13:21:41 2011 +0200
@@ -135,11 +135,6 @@
 
 val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
 
-val symbols_path =
-  [getenv "ISABELLE_HOME", "etc", "symbols"]
-  |> map Path.explode
-  |> Path.appends;
-
 end;
 
 local (* build tables *)
@@ -164,8 +159,7 @@
 fun read_symbols path =
   let
     val parsed_lines =
-      File.read path
-      |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
+      Symbol_Pos.explode (File.read path, Path.position path)
       |> tokenize
       |> filter is_proper
       |> Scan.finite stopper (Scan.repeat line)
@@ -179,7 +173,7 @@
 end;
 
 local
-val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
+val (fromsym, fromabbr, tosym, toabbr) = read_symbols (Path.explode "~~/etc/symbols");
 in
 val symbol_to_unicode = Symtab.lookup fromsym;
 val abbrev_to_unicode = Symtab.lookup fromabbr;