--- 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 ())