--- a/src/Pure/General/file.ML Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/General/file.ML Tue Oct 27 13:16:16 2009 +0100
@@ -90,10 +90,10 @@
Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
in
-fun check_cache (path, time) = CRITICAL (fn () =>
+fun check_cache (path, time) =
(case Symtab.lookup (! ident_cache) path of
NONE => NONE
- | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
+ | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
fun update_cache (path, (time, id)) = CRITICAL (fn () =>
Unsynchronized.change ident_cache