# HG changeset patch
# User haftmann
# Date 1357326299 -3600
# Node ID 07ecb6716df2f7baefb4a208bd9fdda7318b4a55
# Parent  b422a48adc2d7b199bd007cf36d56705bb909216
note to eliminate dynamic name reference

diff -r b422a48adc2d -r 07ecb6716df2 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 04 19:00:49 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 04 20:04:59 2013 +0100
@@ -451,6 +451,7 @@
 
 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 test_goals =
   Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));