# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 39c52a820f6e50e220d5fda9cfee744e344fe6a7
# Parent  8979b2463fc8938054e9ee7e58bf2b39912309dd
removing exception handling now that is caught at some other point;
 tuned message

diff -r 8979b2463fc8 -r 39c52a820f6e src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -155,7 +155,7 @@
       (* FIXME: why decrement size by one? *)
       let
         val _ =
-          Quickcheck.message ctxt ("[Quickcheck-exhaustive] Test " ^
+          Quickcheck.message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
             (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
             "cardinality: " ^ string_of_int card)          
         val (ts, timing) =
diff -r 8979b2463fc8 -r 39c52a820f6e src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -405,9 +405,7 @@
         fun iterate_and_collect (card, size) 0 report = (NONE, report)
           | iterate_and_collect (card, size) j report =
             let
-              val (test_result, single_report) = apsnd Run (single_tester card size) handle Match => 
-                (if Config.get ctxt Quickcheck.quiet then ()
-                 else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
+              val (test_result, single_report) = apsnd Run (single_tester card size)
               val report = collect_single_report single_report report
             in
               case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
@@ -425,13 +423,7 @@
         fun single_tester c s = compile c s |> Random_Engine.run
         fun iterate (card, size) 0 = NONE
           | iterate (card, size) j =
-            let
-              val result = single_tester card size handle Match => 
-                (if Config.get ctxt Quickcheck.quiet then ()
-                 else warning "Exception Match raised during quickcheck"; NONE)
-            in
-              case result of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
-            end
+            case single_tester card size of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
       in
         fn [card, size] => (rpair NONE (iterate (card, size) iterations))
       end