src/Pure/Concurrent/isabelle_thread.ML

 
 structure Exn: EXN =
 struct
   open Exn;
   val capture = capture0;
+  fun capture_body e = capture e ();
 end;
 
 fun expose_interrupt_result () =
   let
     val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ());
     fun main () =
       (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
        Thread.Thread.testInterrupt ());
-    val test = Exn.capture main ();
+    val test = Exn.capture_body main;
     val _ = Thread_Attributes.set_attributes orig_atts;
   in test end;
 
 val expose_interrupt = Exn.release o expose_interrupt_result;
 

   Thread_Attributes.uninterruptible_body (fn run =>
     run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn);
 
 fun try_finally e f =
   Thread_Attributes.uninterruptible_body (fn run =>
-    Exn.release (Exn.capture (run e) () before f ()));
+    Exn.release (Exn.capture_body (run e) before f ()));
 
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();
 
 end;