src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42159 234ec7011e5d
parent 42090 ef566ce50170
child 42184 1d4fae76ba5e
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 29 23:46:46 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 30 09:44:16 2011 +0200
     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 * term list -> int -> term list option * Quickcheck.report option
     1.8 +    Proof.context -> term * term list -> int list -> 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 @@ -212,7 +212,7 @@
    1.13      list_abs (names ~~ Ts', t'')
    1.14    end
    1.15  
    1.16 -fun compile_generator_expr ctxt (t, eval_terms) 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' = list_abs_free (Term.add_frees t [], t)
    1.21 @@ -221,7 +221,7 @@
    1.22        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.23      val result = dynamic_value_strict
    1.24        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.25 -      thy (Option.map o map) (ensure_testable t'') [] size
    1.26 +      thy (Option.map o map) (ensure_testable t'') []
    1.27    in
    1.28      (result, NONE)
    1.29    end;