--- 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)