# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID b3db5697aab41cc5550f43417f944677e1ea91f5
# Parent  1332f6e856b91ea0cf2ef3c1c45fc6f49ed0c2d1
removed interrupt handling that violates Isabelle/ML exception model

diff -r 1332f6e856b9 -r b3db5697aab4 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -261,7 +261,6 @@
         | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
       handle TimeLimit.TimeOut =>
         error (excipit "ran out of time")
-     | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
   in
     (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   end;