execute/system: non-critical;
authorwenzelm
Fri, 05 Oct 2007 20:10:35 +0200
changeset 24858 a3a81e73f552
parent 24857 2dde4189a055
child 24859 9b9b1599fb89
execute/system: non-critical;
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;