src/Pure/General/secure.ML
changeset 24858 a3a81e73f552
parent 24663 015a8838e656
child 25188 a342dec991aa
--- 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;