# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 99a4ef20704df79e04f7d54e9c510923ea52e98c
# Parent  1108529100cea92f733f47a411dc12d1ffabdf89
renamed generator into exhaustive

diff -r 1108529100ce -r 99a4ef20704d src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -289,6 +289,6 @@
     (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   #> setup_smart_quantifier
   #> Context.theory_map
-    (Quickcheck.add_generator ("small", compile_generator_expr));
+    (Quickcheck.add_generator ("exhaustive", compile_generator_expr));
 
 end;