explicit references avoid dynamic lookup
authorhaftmann
Fri Jan 11 08:17:47 2013 +0100 (2013-01-11)
changeset 508185d4852f1b952
parent 50817 652731d92061
child 50820 e8d641235191
child 50821 95a61264a6ab
child 50831 7784cc660580
explicit references avoid dynamic lookup
src/HOL/Tools/Quickcheck/random_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 11 08:17:39 2013 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 11 08:17:47 2013 +0100
     1.3 @@ -449,9 +449,11 @@
     1.4        end
     1.5    end;
     1.6  
     1.7 -fun size_matters_for _ Ts = not (forall
     1.8 -  (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
     1.9 -    (*FIXME eliminate dynamic name reference*)
    1.10 +val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2},
    1.11 +  @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}];
    1.12 +
    1.13 +fun size_matters_for _ Ts =
    1.14 +  not (forall (fn Type (tyco, []) => member (op =) size_types tyco | _ => false) Ts);
    1.15  
    1.16  val test_goals =
    1.17    Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));