author | wenzelm |
Fri, 05 Oct 2007 20:10:35 +0200 | |
changeset 24858 | a3a81e73f552 |
parent 24857 | 2dde4189a055 |
child 24859 | 9b9b1599fb89 |
--- 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;