src/Pure/Concurrent/isabelle_thread.ML

   val join: T -> unit
   val interrupt: exn
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  structure Exn: EXN
   val expose_interrupt_result: unit -> unit Exn.result
   val expose_interrupt: unit -> unit  (*exception Interrupt*)
   val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
   val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
   val try: (unit -> 'a) -> 'a option

 fun interrupt_self () = raise interrupt;
 
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+structure Exn: EXN =
+struct
+  open Exn;
+  val capture = capture0;
+end;
+
 fun expose_interrupt_result () =
   let
     val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
     val _ = Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
     val test = Exn.capture Thread.Thread.testInterrupt ();

 
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();
 
 end;
+
+structure Exn = Isabelle_Thread.Exn;