diff -r 5e40c152c396 -r bd6515e113b2 src/HOL/Tools/Quickcheck/random_generators.ML
--- 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 =