# HG changeset patch
# User wenzelm
# Date 1191607835 -7200
# Node ID a3a81e73f552a9f192d119cfa8c5111f8b6ba19d
# Parent  2dde4189a055c02eddeafba053e9b19a28f6b1b9
execute/system: non-critical;

diff -r 2dde4189a055 -r a3a81e73f552 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Fri Oct 05 20:10:33 2007 +0200
+++ b/src/Pure/General/secure.ML	Fri Oct 05 20:10:35 2007 +0200
@@ -62,8 +62,8 @@
 val orig_execute = execute;
 val orig_system = system;
 
-fun execute s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_execute s));
-fun system s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_system s));
+fun execute s = (secure_shell (); orig_execute s);
+fun system s = (secure_shell (); orig_system s);
 
 end;