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.
more robust exception handling
authorblanchet
Wed, 03 Sep 2014 22:47:05 +0200
changeset 58164 c54510cfe933
parent 58163 c1e32fe387f4
child 58165 2ec97d9c1e83
more robust exception handling
src/HOL/Library/Countable.thy file | annotate | diff | comparison | revisions 
--- 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 =
isabelle