src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42028 bd6515e113b2
parent 42027 5e40c152c396
child 42039 cef738d55348
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -216,12 +216,13 @@
 fun compile_generator_expr ctxt (t, eval_terms) size =
   let
     val thy = ProofContext.theory_of ctxt
-    val t' = if Config.get ctxt finite_functions then finitize_functions t else t
+    val t' = list_abs_free (Term.add_frees t [], t)
+    val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
     fun ensure_testable t =
       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
     val result = dynamic_value_strict
       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
-      thy (Option.map o map) (ensure_testable t') [] size
+      thy (Option.map o map) (ensure_testable t'') [] size
   in
     (result, NONE)
   end;