| 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;