reraise interrupts as usual;
authorwenzelm
Wed, 12 Jan 2011 15:08:21 +0100
changeset 41520 3470b54e95d6
parent 41519 0940fff556a6
child 41521 c704c437ec74
reraise interrupts as usual;
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