src/Tools/quickcheck.ML
changeset 40381 96c37a685a13
parent 40366 a2866dbfbe6b
child 40643 3bba5e71a873
--- a/src/Tools/quickcheck.ML	Fri Nov 05 19:39:25 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Nov 05 19:47:20 2010 +0100
@@ -239,7 +239,7 @@
         | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
       handle TimeLimit.TimeOut =>
         error (excipit "ran out of time")
-     | Exn.Interrupt => error (excipit "was interrupted")
+     | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
   in
     (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
   end;