diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Mar 30 09:44:16 2011 +0200
@@ -39,7 +39,7 @@
   val write_program : logic_program -> string
   val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
   
-  val quickcheck : Proof.context -> term * term list -> int -> term list option * Quickcheck.report option
+  val quickcheck : Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
 
   val trace : bool Unsynchronized.ref
   
@@ -1009,7 +1009,7 @@
 
 (* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
 
-fun quickcheck ctxt (t, []) size =
+fun quickcheck ctxt [(t, [])] [_, size] =
   let
     val t' = list_abs_free (Term.add_frees t [], t)
     val options = code_options_of (ProofContext.theory_of ctxt)