note to eliminate dynamic name reference
authorhaftmann
Fri, 04 Jan 2013 20:04:59 +0100
changeset 50723 07ecb6716df2
parent 50722 b422a48adc2d
child 50731 72624ff45676
note to eliminate dynamic name reference
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));