# HG changeset patch # User bulwahn # Date 1329899701 -3600 # Node ID d3bcc356cc60719f2b11035d3550743b48a2f319 # Parent abbec6fa25c8e94d1c22e40641443d9b744f956d preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work) diff -r abbec6fa25c8 -r d3bcc356cc60 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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