src/HOL/Mirabelle/Tools/mirabelle.ML
changeset 39232 69c6d3e87660
parent 36787 f60e4dd6d76f
child 39377 9e544eb396dc
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -73,12 +73,12 @@
     1.4  fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
     1.5  
     1.6  fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
     1.7 -  handle (exn as Exn.Interrupt) => reraise exn
     1.8 -       | exn => (log_exn log tag id exn; ())
     1.9 +  handle exn =>
    1.10 +    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
    1.11  
    1.12  fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
    1.13 -  handle (exn as Exn.Interrupt) => reraise exn
    1.14 -       | exn => (log_exn log tag id exn; d)
    1.15 +  handle exn =>
    1.16 +    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
    1.17  
    1.18  fun register (init, run, done) thy =
    1.19    let val id = length (Actions.get thy) + 1