diff -r f42665561801 -r 81aafd465662 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/source.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -114,7 +114,7 @@
 
 (* stream source *)
 
-fun slurp_input instream = CRITICAL (fn () =>
+fun slurp_input instream = NAMED_CRITICAL "IO" (fn () =>
   let
     fun slurp () =
       (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
@@ -128,7 +128,7 @@
     if exists (fn c => c = "\n") input then (input, ())
     else
       (case
-        CRITICAL (fn () =>
+        NAMED_CRITICAL "IO" (fn () =>
           (TextIO.output (outstream, Output.output prompt);
             TextIO.flushOut outstream;
             TextIO.inputLine instream)) of