diff -r abd1f074cb98 -r eeb10fdd9535 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200 @@ -442,10 +442,12 @@ (** setup **) +val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false); + val setup = Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype)) #> Code_Target.extend_target (target, (Code_Runtime.target, K I)) - #> Context.theory_map (Quickcheck.add_tester ("random", test_goals)); + #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals))); end;