changeset 78672 | fcdfd3251892 |
parent 74844 | 90242c744a1a |
child 78681 | 38fe769658be |
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 19 13:02:48 2023 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 19 13:12:13 2023 +0200 @@ -1049,7 +1049,7 @@ in if not (null ps) orelse rc = 0 then Normal (ps, js, first_error) else if rc = 2 then TimedOut js - else if rc = 130 then raise Exn.Interrupt + else if rc = 130 then Exn.interrupt () else Error (if first_error = "" then "Unknown error" else first_error, js) end end