--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -377,16 +377,17 @@
fun compile_generator_expr ctxt (t, eval_terms) =
let
- val Ts = (map snd o fst o strip_abs) t;
+ val t' = list_abs_free (Term.add_frees t [], t)
+ val Ts = (map snd o fst o strip_abs) t';
val thy = ProofContext.theory_of ctxt
val iterations = Config.get ctxt Quickcheck.iterations
in
if Config.get ctxt Quickcheck.report then
let
- val t' = mk_reporting_generator_expr thy t Ts;
+ val t'' = mk_reporting_generator_expr thy t' Ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t'' [];
val single_tester = compile #> Random_Engine.run
fun iterate_and_collect size 0 report = (NONE, report)
| iterate_and_collect size j report =
@@ -404,10 +405,10 @@
end
else
let
- val t' = mk_generator_expr thy t Ts;
+ val t'' = mk_generator_expr thy t' Ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t'' [];
val single_tester = compile #> Random_Engine.run
fun iterate size 0 = NONE
| iterate size j =