tuned;

--- a/src/Pure/System/scala.ML	Tue Sep 19 19:48:54 2023 +0200
+++ b/src/Pure/System/scala.ML	Tue Sep 19 20:24:39 2023 +0200
@@ -35,7 +35,7 @@
           | ("1", _) => Exn.Res rest
           | ("2", [msg]) => Exn.Exn (ERROR (Bytes.content msg))
           | ("3", [msg]) => Exn.Exn (Fail (Bytes.content msg))
-          | ("4", []) => Exn.Exn Exn.Interrupt
+          | ("4", []) => Exn.interrupt_exn
           | _ => raise Fail "Malformed Scala.result");
       in Synchronized.change results (Symtab.map_entry (Bytes.content id) (K result)) end);
 
@@ -57,7 +57,7 @@
             (case Symtab.lookup tab id of
               SOME (Exn.Exn Match) => NONE
             | SOME result => SOME (result, Symtab.delete id tab)
-            | NONE => SOME (Exn.Exn Exn.Interrupt, tab)));
+            | NONE => SOME (Exn.interrupt_exn, tab)));
     in
       invoke ();
       Exn.release (restore_attributes await_result ())