diff -r f42665561801 -r 81aafd465662 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/secure.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -40,10 +40,10 @@
 val orig_use_text = use_text;
 val orig_use_file = use_file;
 
-fun use_text name pr verbose txt = CRITICAL (fn () =>
+fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
   (secure_mltext (); orig_use_text name pr verbose txt));
 
-fun use_file pr verbose name = CRITICAL (fn () =>
+fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () =>
   (secure_mltext (); orig_use_file pr verbose name));
 
 fun use name = use_file Output.ml_output true name;
@@ -62,8 +62,8 @@
 val orig_execute = execute;
 val orig_system = system;
 
-fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s));
-fun system s = CRITICAL (fn () => (secure_shell (); orig_system s));
+fun execute s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_execute s));
+fun system s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_system s));
 
 end;