src/HOL/Library/Countable.thy

--- a/src/HOL/Library/Countable.thy	Wed Sep 03 22:46:54 2014 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Sep 03 22:47:05 2014 +0200
@@ -204,7 +204,8 @@
 ML {*
 fun countable_datatype_tac ctxt st =
   HEADGOAL (old_countable_datatype_tac ctxt) st
-  handle ERROR _ => BNF_LFP_Countable.countable_datatype_tac ctxt st;
+  handle exn =>
+    if Exn.is_interrupt exn then reraise exn else BNF_LFP_Countable.countable_datatype_tac ctxt st;
 
 (* compatibility *)
 fun countable_tac ctxt =