--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Jan 25 09:50:34 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Jan 25 15:19:04 2012 +0100
@@ -455,7 +455,11 @@
end
end;
-val test_goals = Quickcheck_Common.generator_test_goal_terms ("random", compile_generator_expr);
+fun size_matters_for _ Ts = not (forall
+ (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
+
+val test_goals =
+ Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
(** setup **)