# HG changeset patch # User bulwahn # Date 1301048341 -3600 # Node ID d1c761375a750ebda695f352077acadf3e1bacf1 # Parent 17e0cd9bc259539652ca3971bf2ae7723653bbb7 revisiting Code_Prolog (cf. 6fe4abb9437b) diff -r 17e0cd9bc259 -r d1c761375a75 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 25 11:19:00 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 25 11:19:01 2011 +0100 @@ -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 -> int -> term list option * Quickcheck.report option + val quickcheck : Proof.context -> term * term list -> int -> term list option * Quickcheck.report option val trace : bool Unsynchronized.ref