src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42027 5e40c152c396
parent 42024 51df23535105
child 42028 bd6515e113b2
     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 @@ -7,7 +7,7 @@
     1.4  signature NARROWING_GENERATORS =
     1.5  sig
     1.6    val compile_generator_expr:
     1.7 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.8 +    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
     1.9    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    1.10    val finite_functions : bool Config.T
    1.11    val setup: theory -> theory
    1.12 @@ -213,7 +213,7 @@
    1.13      list_abs (names ~~ Ts', t'')
    1.14    end
    1.15  
    1.16 -fun compile_generator_expr ctxt t size =
    1.17 +fun compile_generator_expr ctxt (t, eval_terms) size =
    1.18    let
    1.19      val thy = ProofContext.theory_of ctxt
    1.20      val t' = if Config.get ctxt finite_functions then finitize_functions t else t