File.read/write/append: non-critical (basic IO operations already thread-safe);

--- a/src/Pure/General/file.ML	Mon Aug 20 20:43:59 2007 +0200
+++ b/src/Pure/General/file.ML	Mon Aug 20 20:44:00 2007 +0200
@@ -129,14 +129,14 @@
 
 in
 
-fun read path = NAMED_CRITICAL "IO" (fn () =>
-  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
+fun read path =
+  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
 
-fun write_list path txts = NAMED_CRITICAL "IO" (fn () =>
-  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
+fun write_list path txts =
+  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
 
-fun append_list path txts = NAMED_CRITICAL "IO" (fn () =>
-  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
+fun append_list path txts =
+  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];