# HG changeset patch
# User wenzelm
# Date 1422187116 -3600
# Node ID 94194354e00414c06ee4d09b6c98950f584d13c0
# Parent  9da5b2c61049cc199ddfa884adab4f447fee57b7
tuned;

diff -r 9da5b2c61049 -r 94194354e004 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 24 22:00:24 2015 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Jan 25 12:58:36 2015 +0100
@@ -289,12 +289,10 @@
                     (counterexample, !current_result)
                   else
                     let
-                      val cex = Option.map (rpair []) (counterexample_of counterexample)
-                    in
-                      (message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
-                      message "Quickcheck continues to find a genuine counterexample...";
-                      with_size true (k + 1))
-                    end
+                      val cex = Option.map (rpair []) (counterexample_of counterexample);
+                      val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+                      val _ = message "Quickcheck continues to find a genuine counterexample...";
+                    in with_size true (k + 1) end
                end
             end
       in with_size genuine_only 0 end
@@ -471,7 +469,7 @@
             evaluation_terms = Option.map (K []) counterexample,
             timings = #timings (dest_result result), reports = #reports (dest_result result)}
         | NONE =>
-          (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
+          (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
            Quickcheck.empty_result)
       end
     else
@@ -501,7 +499,7 @@
               timings = #timings (dest_result result),
               reports = #reports (dest_result result)}
         | NONE =>
-          (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
+          (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
            Quickcheck.empty_result)
       end
   end;
@@ -509,7 +507,7 @@
 fun test_goals ctxt catch_code_errors insts goals =
   if (not (getenv "ISABELLE_GHC" = "")) then
     let
-      val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
+      val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing...";
       val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     in
       Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)