diff -r a434f89a9962 -r a549ff1d4070 src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 08 16:47:57 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 08 18:07:03 2010 +0100
@@ -81,7 +81,10 @@
 
 fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
- 
+
+fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+  --> @{typ "Code_Evaluation.term list option"}
+
 fun mk_equations thy descr vs tycos smalls (Ts, Us) =
   let
     fun mk_small_call T =
@@ -217,6 +220,7 @@
 
 fun mk_smart_generator_expr ctxt t =
   let
+    val thy = ProofContext.theory_of ctxt
     val ((vnames, Ts), t') = apfst split_list (strip_abs t)
     val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
     val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
@@ -229,9 +233,14 @@
     val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
     val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
     fun mk_small_closure (free as Free (_, T), term_var) t =
-      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
-        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
-          $ lambda free (lambda term_var t)) $ depth
+      if Sign.of_sort thy (T, @{sort enum}) then
+        Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T)
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
+            $ lambda free (lambda term_var t))
+      else
+        Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
+            $ lambda free (lambda term_var t)) $ depth
     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
     val none_t = @{term "None :: term list option"}
     fun mk_safe_if (cond, then_t, else_t) =