# HG changeset patch
# User haftmann
# Date 1357888667 -3600
# Node ID 5d4852f1b952aff0729bc5a0ca04e414cdac6059
# Parent  652731d920614d72b054f3682a69b015920b2b05
explicit references avoid dynamic lookup

diff -r 652731d92061 -r 5d4852f1b952 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 11 08:17:39 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 11 08:17:47 2013 +0100
@@ -449,9 +449,11 @@
       end
   end;
 
-fun size_matters_for _ Ts = not (forall
-  (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
-    (*FIXME eliminate dynamic name reference*)
+val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2},
+  @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}];
+
+fun size_matters_for _ Ts =
+  not (forall (fn Type (tyco, []) => member (op =) size_types tyco | _ => false) Ts);
 
 val test_goals =
   Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));