--- a/src/HOL/Tools/inductive_codegen.ML Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Sep 09 17:23:03 2010 +0200
@@ -9,7 +9,7 @@
val add : string option -> int option -> attribute
val test_fn : (int * int * int -> term list option) Unsynchronized.ref
val test_term:
- Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * (bool list * bool)
val setup : theory -> theory
val quickcheck_setup : theory -> theory
end;
@@ -799,7 +799,7 @@
val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
-fun test_term ctxt report t =
+fun test_term ctxt t =
let
val thy = ProofContext.theory_of ctxt;
val (xs, p) = strip_abs t;