preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Feb 22 08:05:28 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Feb 22 09:35:01 2012 +0100
@@ -512,7 +512,7 @@
(* setup *)
-val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
+val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
val setup =
Code.datatype_interpretation ensure_partial_term_of