# HG changeset patch
# User wenzelm
# Date 1294841301 -3600
# Node ID 3470b54e95d6c3c28cd06c17ff05b03a816dcb51
# Parent  0940fff556a6372ff38ca2e4aa0151c9aae392fa
reraise interrupts as usual;

diff -r 0940fff556a6 -r 3470b54e95d6 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Jan 12 15:07:29 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Jan 12 15:08:21 2011 +0100
@@ -178,7 +178,7 @@
   end
   handle TimeLimit.TimeOut => "TIMEOUT"
        | NOT_SUPPORTED _ => "UNSUP"
-       | _ => "UNKNOWN"
+       | exn => if Exn.is_interrupt then reraise exn else "UNKNOWN"
 
 fun check_theory thy =
   let