src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43878 eeb10fdd9535
parent 43850 7f2cbc713344
child 43891 4690f76f327a
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -461,11 +461,13 @@
     1.4  
     1.5  (* setup *)
     1.6  
     1.7 +val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K true);
     1.8 +
     1.9  val setup =
    1.10    Code.datatype_interpretation ensure_partial_term_of
    1.11    #> Code.datatype_interpretation ensure_partial_term_of_code
    1.12    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    1.13      (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
    1.14 -  #> Context.theory_map (Quickcheck.add_tester ("narrowing", test_goals))
    1.15 +  #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
    1.16      
    1.17  end;
    1.18 \ No newline at end of file