# HG changeset patch
# User wenzelm
# Date 1300029254 -3600
# Node ID 8e32c3992cb3e51a564f8f459704d84fa9fc83ca
# Parent  b97091ae583ab810af14f013b8e2f75ea7a4aa49
more conventional variable name;

diff -r b97091ae583a -r 8e32c3992cb3 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Sun Mar 13 16:01:00 2011 +0100
+++ b/src/Tools/cache_io.ML	Sun Mar 13 16:14:14 2011 +0100
@@ -84,7 +84,7 @@
 
 fun make path =
   let val table = if File.exists path then load path else (1, Symtab.empty)
-  in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
+  in Cache {path=path, table=Synchronized.var "Cache_IO" table} end
 
 fun load_cached_result cache_path (p, len1, len2) =
   let