# HG changeset patch
# User wenzelm
# Date 1428833268 -7200
# Node ID b2acd53016158446647cd79dd6dfa119c4f71f41
# Parent  9a06e10f1a5ce019119caaaad78e51a493f4cf20
tuned -- avoid ML warnings;

diff -r 9a06e10f1a5c -r b2acd5301615 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sun Apr 12 11:38:05 2015 +0200
+++ b/src/HOL/Library/Countable.thy	Sun Apr 12 12:07:48 2015 +0200
@@ -202,9 +202,9 @@
 
 ML {*
 fun countable_datatype_tac ctxt st =
-  HEADGOAL (old_countable_datatype_tac ctxt) st
-  handle exn =>
-    if Exn.is_interrupt exn then reraise exn else BNF_LFP_Countable.countable_datatype_tac ctxt st;
+  (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of
+    SOME res => res
+  | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st);
 
 (* compatibility *)
 fun countable_tac ctxt =