diff -r d86540f6ea0d -r becf5d5187cc src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/cache_io.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -81,7 +81,7 @@
       File.shell_path cache_path)
 
     fun int_of_string s =
-      (case read_int (explode s) of
+      (case read_int (raw_explode s) of
         (i, []) => i
       | _ => err ())