src/Pure/Concurrent/isabelle_thread.scala

     def apply(thread: Isabelle_Thread) { handle(thread) }
     override def toString: String = name
   }
 
   def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A =
-    self.interrupt_handler(handler)(body)
+    if (handler == null) body
+    else self.interrupt_handler(handler)(body)
 
   def interrupt_handler[A](handle: Isabelle_Thread => Unit)(body: => A): A =
     self.interrupt_handler(Interrupt_Handler(handle))(body)
 
   def interruptible[A](body: => A): A =

   @volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible
 
   override def interrupt: Unit = handler(thread)
 
   def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A =
-  {
-    require(is_self)
+    if (new_handler == null) body
+    else {
+      require(is_self)
 
-    val old_handler = handler
-    handler = new_handler
-    try {
-      if (clear_interrupt) interrupt
-      body
+      val old_handler = handler
+      handler = new_handler
+      try {
+        if (clear_interrupt) interrupt
+        body
+      }
+      finally {
+        handler = old_handler
+        if (clear_interrupt) interrupt
+      }
     }
-    finally {
-      handler = old_handler
-      if (clear_interrupt) interrupt
-    }
-  }
 }