src/HOL/Tools/Quickcheck/random_generators.ML
changeset 46331 f5598b604a54
parent 45940 71970a26a269
child 46547 d1dcb91a512e
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Jan 25 09:50:34 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Jan 25 15:19:04 2012 +0100
     1.3 @@ -455,7 +455,11 @@
     1.4        end
     1.5    end;
     1.6  
     1.7 -val test_goals = Quickcheck_Common.generator_test_goal_terms ("random", compile_generator_expr);
     1.8 +fun size_matters_for _ Ts = not (forall
     1.9 +  (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
    1.10 +
    1.11 +val test_goals =
    1.12 +  Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
    1.13    
    1.14  (** setup **)
    1.15