src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42027 5e40c152c396
parent 42024 51df23535105
child 42028 bd6515e113b2
--- 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
@@ -7,7 +7,7 @@
 signature NARROWING_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> term -> int -> term list option * Quickcheck.report option
+    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
   val finite_functions : bool Config.T
   val setup: theory -> theory
@@ -213,7 +213,7 @@
     list_abs (names ~~ Ts', t'')
   end
 
-fun compile_generator_expr ctxt t size =
+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