--- 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)