diff -r cb31c89387be -r 14efbc20b708 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 22:12:40 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 14:05:13 2009 +0200
@@ -70,13 +70,13 @@
 
 fun log_sep thy = log thy "------------------"
 
-fun try_with f NONE = SOME ()
-  | try_with f (SOME e) = (f e; try (fn () => reraise e) ())
+fun log_exn thy name (exn : exn) = log thy ("Unhandled exception in action " ^
+  quote name ^ ":\n" ^ PolyML.makestring exn)
 
-fun capture_exns thy name f x =
-  (case try_with I (Exn.get_exn (Exn.capture f x)) of
-    NONE => (log thy ("Unhandled exception in " ^ quote name); log_sep thy)
-  | SOME _ => log_sep thy)
+fun try_with f g x = SOME (g x)
+  handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; NONE)
+
+fun capture_exns thy name f x = (try_with (log_exn thy name) f x; log_sep thy)
 
 fun apply_actions thy info (pre, post, time) actions =
   let