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