# HG changeset patch
# User bulwahn
# Date 1323084963 -3600
# Node ID f8cc1f6528fb30a23a0cc19f698059bf8eb931b4
# Parent  6210c350d88bb906fca5aff6f6f299cb5b74e0eb
NEWS

diff -r 6210c350d88b -r f8cc1f6528fb NEWS
--- a/NEWS	Mon Dec 05 12:36:02 2011 +0100
+++ b/NEWS	Mon Dec 05 12:36:03 2011 +0100
@@ -145,6 +145,21 @@
 produces a rule which can be used to perform case distinction on both
 a list and a nat.
 
+* Quickcheck:
+  - Quickcheck returns variable assignments as counterexamples, which
+    allows to reveal the underspecification of functions under test.
+    For example, refuting "hd xs = x", it presents the variable
+    assignment xs = [] and x = a1 as a counterexample, assuming that
+    any property is false whenever "hd []" occurs in it.
+    These counterexample are marked as potentially spurious, as
+    Quickcheck also returns "xs = []" as a counterexample to the
+    obvious theorem "hd xs = hd xs".
+    After finding a potentially spurious counterexample, Quickcheck
+    continues searching for genuine ones.
+    By default, Quickcheck shows potentially spurious and genuine
+    counterexamples. The option "genuine_only" sets quickcheck to
+    only show genuine counterexamples.
+ 
 * Nitpick:
   - Fixed infinite loop caused by the 'peephole_optim' option and
     affecting 'rat' and 'real'.
diff -r 6210c350d88b -r f8cc1f6528fb src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 12:36:02 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 12:36:03 2011 +0100
@@ -372,8 +372,9 @@
 
 val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   ((mk_generator_expr, 
-    absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"}),
-    @{typ "code_numeral => Random.seed => (bool * term list) option * Random.seed"})
+    absdummy @{typ bool} (absdummy @{typ code_numeral}
+      @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"})),
+    @{typ "bool => code_numeral => Random.seed => (bool * term list) option * Random.seed"})
 
 val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   ((mk_reporting_generator_expr,