src/HOL/Tools/smallvalue_generators.ML
changeset 40913 99a4ef20704d
parent 40911 7febf76e0a69
child 41085 a549ff1d4070
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -289,6 +289,6 @@
     1.4      (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
     1.5    #> setup_smart_quantifier
     1.6    #> Context.theory_map
     1.7 -    (Quickcheck.add_generator ("small", compile_generator_expr));
     1.8 +    (Quickcheck.add_generator ("exhaustive", compile_generator_expr));
     1.9  
    1.10  end;