diff -r 66e7a3131fe3 -r fcdfd3251892 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Tue Sep 19 13:02:48 2023 +0200 +++ b/src/Pure/System/isabelle_system.ML Tue Sep 19 13:12:13 2023 +0200 @@ -68,7 +68,7 @@ if head = Bash.server_uuid andalso length args = 1 then loop (SOME (hd args)) s else if head = Bash.server_interrupt andalso null args then - raise Exn.Interrupt + Exn.interrupt () else if head = Bash.server_failure andalso length args = 1 then raise Fail (hd args) else if head = Bash.server_result andalso length args >= 4 then