Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned -- avoid ML warnings;
authorwenzelm
Sun, 12 Apr 2015 12:07:48 +0200
changeset 60029 b2acd5301615
parent 60028 9a06e10f1a5c
child 60030 9f5b287279c8
tuned -- avoid ML warnings;
src/HOL/Library/Countable.thy file | annotate | diff | comparison | revisions 
--- 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 =
isabelle