# HG changeset patch # User bulwahn # Date 1311142593 -7200 # Node ID 575bf39e078b90682424d828e172d53ffdb4dfbf # Parent 7feb72f7bc3e546422e9859a33e0ba9ee3e25b5d making messages more informative diff -r 7feb72f7bc3e -r 575bf39e078b src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jul 20 08:16:32 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jul 20 08:16:33 2011 +0200 @@ -263,7 +263,7 @@ (NONE, !current_result) else let - val _ = message ("Test data size: " ^ string_of_int k) + val _ = message ("[Quickcheck-Narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))